From 9a63fdf0cad004d21ff9e937b08e7758e304bcd3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Jul 2016 11:40:52 +0200 Subject: [PATCH 1/5] Adding "eassert", "eenough", "epose proof", which allow to state a goal with unresolved evars. --- plugins/ltac/g_tactic.ml4 | 27 +++++++++++++++++++++------ plugins/ltac/pptactic.ml | 8 ++++---- plugins/ltac/tacexpr.mli | 2 +- plugins/ltac/tacintern.ml | 4 ++-- plugins/ltac/tacinterp.ml | 18 +++++++++--------- plugins/ltac/tacsubst.ml | 4 ++-- 6 files changed, 39 insertions(+), 24 deletions(-) diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 1404b1c1f10d..c6a3beb89683 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -552,24 +552,39 @@ GEXTEND Gram (* Alternative syntax for "pose proof c as id" *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; c = lconstr; ")" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + c = lconstr; ")" -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "assert c as id by tac" *) | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "enough c as id by tac" *) | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c)) + | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c)) | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c)) + | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c)) | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c)) + | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c)) | IDENT "generalize"; c = constr -> TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)]) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index a001c6a2ba60..22ecf61aa2f9 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -768,15 +768,15 @@ type 'a extra_genarg_printer = primitive "cofix" ++ spc () ++ pr_id id ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l ) - | TacAssert (b,Some tac,ipat,c) -> + | TacAssert (ev,b,Some tac,ipat,c) -> hov 1 ( - primitive (if b then "assert" else "enough") ++ + primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac ) - | TacAssert (_,None,ipat,c) -> + | TacAssert (ev,_,None,ipat,c) -> hov 1 ( - primitive "pose proof" + primitive (if ev then "epose proof" else "pose proof") ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ) | TacGeneralize l -> diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index bf760e7bba31..11e7278d9200 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -141,7 +141,7 @@ type 'a gen_atomic_tactic_expr = | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of - bool * 'tacexpr option option * + evars_flag * bool * 'tacexpr option option * 'dtrm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index e431a13bc211..734ce46e4831 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -489,8 +489,8 @@ let rec intern_atomic lf ist x = | TacMutualCofix (id,l) -> let f (id,c) = (intern_ident lf ist id,intern_type ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) - | TacAssert (b,otac,ipat,c) -> - TacAssert (b,Option.map (Option.map (intern_pure_tactic ist)) otac, + | TacAssert (ev,b,otac,ipat,c) -> + TacAssert (ev,b,Option.map (Option.map (intern_pure_tactic ist)) otac, Option.map (intern_intro_pattern lf ist) ipat, intern_constr_gen false (not (Option.is_empty otac)) ist c) | TacGeneralize cl -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a9ec779d1139..d4ed77015323 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -672,10 +672,7 @@ let pure_open_constr_flags = { expand_evars = false } (* Interprets an open constr *) -let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c = - let flags = - if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags () - else open_constr_use_classes_flags () in +let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c = interp_gen expected_type ist false flags env sigma c let interp_pure_open_constr ist = @@ -1727,18 +1724,21 @@ and interp_atomic ist tac : unit Proofview.tactic = Sigma.Unsafe.of_pair (tac, sigma) end } end - | TacAssert (b,t,ipat,c) -> + | TacAssert (ev,b,t,ipat,c) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let (sigma,c) = - (if Option.is_empty t then interp_constr else interp_type) ist env sigma c + let (sigma,c) = + let expected_type = + if Option.is_empty t then WithoutTypeConstraint else IsType in + let flags = open_constr_use_classes_flags () in + interp_open_constr ~expected_type ~flags ist env sigma c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in let tac = Option.map (Option.map (interp_tactic ist)) t in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES ev (name_atomic ~env - (TacAssert(b,Option.map (Option.map ignore) t,ipat,c)) + (TacAssert(ev,b,Option.map (Option.map ignore) t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma end } | TacGeneralize cl -> diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 4390ff08b465..1ae792971c69 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -146,8 +146,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) - | TacAssert (b,otac,na,c) -> - TacAssert (b,Option.map (Option.map (subst_tactic subst)) otac,na, + | TacAssert (ev,b,otac,na,c) -> + TacAssert (ev,b,Option.map (Option.map (subst_tactic subst)) otac,na, subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) From be73d7eccd3e3165ce719b36910920e05cf416bc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Jul 2016 11:53:37 +0200 Subject: [PATCH 2/5] Adding "epose", "eset", "eremember" which allow to set terms with evars. This is for consistency with the rest of the language. For instance, "eremember" and "epose" are supposed to refer to terms occurring in the goal, hence not leaving evars, hence in general pointless. Eventually, I guess that "e" should be a modifier (see e.g. the discussion at #3872), or the difference is removed. --- plugins/ltac/g_tactic.ml4 | 21 ++++++++++++++++----- plugins/ltac/pptactic.ml | 8 ++++---- plugins/ltac/tacexpr.mli | 2 +- plugins/ltac/tacintern.ml | 4 ++-- plugins/ltac/tacinterp.ml | 17 +++++++++-------- plugins/ltac/tacsubst.ml | 4 ++-- tactics/tactics.ml | 4 ++-- tactics/tactics.mli | 2 +- 8 files changed, 37 insertions(+), 25 deletions(-) diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index c6a3beb89683..83bfd0233aaa 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -538,16 +538,27 @@ GEXTEND Gram TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,b,Locusops.nowhere,true,None)) | IDENT "pose"; b = constr; na = as_name -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,b,Locusops.nowhere,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) + | IDENT "epose"; (id,b) = bindings_with_parameters -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) + | IDENT "epose"; b = constr; na = as_name -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,c,p,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,c,p,true,None)) | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None)) + | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) + | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None)) | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; p = clause_dft_all -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,false,e)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e)) + | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat; + p = clause_dft_all -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e)) (* Alternative syntax for "pose proof c as id" *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 22ecf61aa2f9..4e254ea7665f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -786,11 +786,11 @@ type 'a extra_genarg_printer = pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> - hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) - | TacLetTac (na,c,cl,b,e) -> + | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl -> + hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c) + | TacLetTac (ev,na,c,cl,b,e) -> hov 1 ( - (if b then primitive "set" else primitive "remember") ++ + primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++ (if b then pr_pose pr.pr_constr pr.pr_lconstr na c else pr_pose_as_style pr.pr_constr na c) ++ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 11e7278d9200..b78dc374262d 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -144,7 +144,7 @@ type 'a gen_atomic_tactic_expr = evars_flag * bool * 'tacexpr option option * 'dtrm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list - | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * + | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * intro_pattern_naming_expr located option (* Derived basic tactics *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 734ce46e4831..2dc3bb37868c 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -497,9 +497,9 @@ let rec intern_atomic lf ist x = TacGeneralize (List.map (fun (c,na) -> intern_constr_with_occurrences ist c, intern_name lf ist na) cl) - | TacLetTac (na,c,cls,b,eqpat) -> + | TacLetTac (ev,na,c,cls,b,eqpat) -> let na = intern_name lf ist na in - TacLetTac (na,intern_constr ist c, + TacLetTac (ev,na,intern_constr ist c, (clause_app (intern_hyp_location ist) cls),b, (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat)) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d4ed77015323..6b0914ff95d8 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1751,36 +1751,37 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacGeneralize cl) (Tactics.generalize_gen cl)) sigma end } - | TacLetTac (na,c,clp,b,eqpat) -> + | TacLetTac (ev,na,c,clp,b,eqpat) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let clp = interp_clause ist env sigma clp in let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in - if Locusops.is_nowhere clp then + if Locusops.is_nowhere clp (* typically "pose" *) then (* We try to fully-typecheck the term *) - let (sigma,c_interp) = interp_constr ist env sigma c in + let flags = open_constr_use_classes_flags () in + let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in let let_tac b na c cl eqpat = let id = Option.default (Loc.tag IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in Tactics.letin_tac with_eq na c None cl in let na = interp_name ist env sigma na in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES ev (name_atomic ~env - (TacLetTac(na,c_interp,clp,b,eqpat)) + (TacLetTac(ev,na,c_interp,clp,b,eqpat)) (let_tac b na c_interp clp eqpat)) sigma else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = let id = Option.default (Loc.tag IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in - Tactics.letin_pat_tac with_eq na c cl + Tactics.letin_pat_tac ev with_eq na c cl in let (sigma',c) = interp_pure_open_constr ist env sigma c in name_atomic ~env - (TacLetTac(na,c,clp,b,eqpat)) - (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) + (TacLetTac(ev,na,c,clp,b,eqpat)) + (Tacticals.New.tclWITHHOLES ev (let_pat_tac b (interp_name ist env sigma na) (sigma,c) clp eqpat) sigma') end } diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 1ae792971c69..f5e6f05ceecd 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -151,8 +151,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacLetTac (id,c,clp,b,eqpat) -> - TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) + | TacLetTac (ev,id,c,clp,b,eqpat) -> + TacLetTac (ev,id,subst_glob_constr subst c,clp,b,eqpat) (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7e8cb4e63212..f4408d40330b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2756,7 +2756,7 @@ let letin_tac with_eq id c ty occs = Sigma (tac, sigma, p) end } -let letin_pat_tac with_eq id c occs = +let letin_pat_tac with_evars with_eq id c occs = Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -2765,7 +2765,7 @@ let letin_pat_tac with_eq id c occs = let abs = AbstractPattern (false,check,id,c,occs,false) in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in let Sigma (c, sigma, p) = match res with - | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c + | None -> finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma c | Some res -> res in let tac = (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 07a80354270a..0dbcce02c5b3 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -385,7 +385,7 @@ val letin_tac : (bool * intro_pattern_naming) option -> (** Common entry point for user-level "set", "pose" and "remember" *) -val letin_pat_tac : (bool * intro_pattern_naming) option -> +val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option -> Name.t -> (evar_map * constr) -> clause -> unit Proofview.tactic (** {6 Generalize tactics. } *) From 3074967fd01acc5987eb2ea648fcfe32aeca1749 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Jul 2016 12:27:53 +0200 Subject: [PATCH 3/5] Few tests for e-variants of assert, set, remember. --- test-suite/success/forward.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 test-suite/success/forward.v diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v new file mode 100644 index 000000000000..0ed5b524f37b --- /dev/null +++ b/test-suite/success/forward.v @@ -0,0 +1,18 @@ +(* Testing forward reasoning *) + +Goal 0=0. +Fail assert (_ = _). +eassert (_ = _)by reflexivity. +eassumption. +Qed. + +Goal 0=0. +Fail set (S ?[nl]). +eset (S ?[n]). +remember (S ?n) as x. +instantiate (n:=0). +Fail remember (S (S _)). +eremember (S (S ?[x])). +instantiate (x:=0). +reflexivity. +Qed. From 5a86aabf4375b5f6f205dd328454748d2bc1217f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Mar 2017 14:12:29 +0100 Subject: [PATCH 4/5] Documentation for eassert, eenough, epose proof, eset, eremember, epose. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Includes fixes and suggestions from Théo. --- CHANGES | 4 ++++ doc/refman/RefMan-tac.tex | 47 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+) diff --git a/CHANGES b/CHANGES index 30bea7a7b552..8fd71f92477d 100644 --- a/CHANGES +++ b/CHANGES @@ -26,6 +26,10 @@ Tactics now uses type classes and rejects terms with unresolved holes, like entry "constr" does. To get the former behavior use "open_constr_with_bindings" (possible source of incompatibility. +- New e-variants eassert, eenough, epose proof, eset, eremember, epose + which behave like the corresponding variants with no "e" but turn + unresolved implicit arguments into existential variables, on the + shelf, rather than failing. Vernacular Commands diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fc3fdd00250b..def42955ff8e 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1155,6 +1155,15 @@ \subsection{\tt set ( {\ident} := {\term} )} These are the general forms that combine the previous possibilities. +\item {\tt eset ( {\ident$_0$} \nelistnosep{\binder} := {\term} ) in {\occgoalset}}\tacindex{eset}\\ + {\tt eset {\term} in {\occgoalset}} + + While the different variants of \texttt{set} expect that no + existential variables are generated by the tactic, \texttt{eset} + removes this constraint. In practice, this is relevant only when + \texttt{eset} is used as a synonym of \texttt{epose}, i.e. when the + term does not occur in the goal. + \item {\tt remember {\term} as {\ident}}\tacindex{remember} This behaves as {\tt set ( {\ident} := {\term} ) in *} and using a @@ -1170,6 +1179,15 @@ \subsection{\tt set ( {\ident} := {\term} )} This is a more general form of {\tt remember} that remembers the occurrences of {\term} specified by an occurrences set. +\item + {\tt eremember {\term} as {\ident}}\tacindex{eremember}\\ + {\tt eremember {\term} as {\ident} in {\occgoalset}}\\ + {\tt eremember {\term} as {\ident} eqn:{\ident}} + + While the different variants of \texttt{remember} expect that no + existential variables are generated by the tactic, \texttt{eremember} + removes this constraint. + \item {\tt pose ( {\ident} := {\term} )}\tacindex{pose} This adds the local definition {\ident} := {\term} to the current @@ -1187,6 +1205,14 @@ \subsection{\tt set ( {\ident} := {\term} )} This behaves as {\tt pose ( {\ident} := {\term} )} but {\ident} is generated by {\Coq}. +\item {\tt epose ( {\ident} := {\term} )}\tacindex{epose}\\ + {\tt epose ( {\ident} \nelistnosep{\binder} := {\term} )}\\ + {\tt epose {\term}} + + While the different variants of \texttt{pose} expect that no + existential variables are generated by the tactic, \texttt{epose} + removes this constraint. + \end{Variants} \subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term} @@ -1284,6 +1310,14 @@ \subsection{\tt assert ( {\ident} :\ {\form} )} \ErrMsg \errindex{Variable {\ident} is already declared} +\item \texttt{eassert {\form} as {\intropattern} by {\tac}}\tacindex{eassert}\tacindex{eassert as}\tacindex{eassert by}\\ + {\tt assert ( {\ident} := {\term} )} + + While the different variants of \texttt{assert} expect that no + existential variables are generated by the tactic, \texttt{eassert} + removes this constraint. This allows not to specify the asserted + statement completely before starting to prove it. + \item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}} This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by @@ -1294,6 +1328,11 @@ \subsection{\tt assert ( {\ident} :\ {\form} )} as {\intropattern}} is the same as applying the {\intropattern} to {\term}. +\item \texttt{epose proof {\term} \zeroone{as {\intropattern}}\tacindex{epose proof}} + + While \texttt{pose proof} expects that no existential variables are generated by the tactic, + \texttt{epose proof} removes this constraint. + \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough} This adds a new hypothesis of name {\ident} asserting {\form} to the @@ -1320,6 +1359,14 @@ \subsection{\tt assert ( {\ident} :\ {\form} )} destructed. If the \texttt{as} {\intropattern} clause generates more than one subgoal, {\tac} is applied to all of them. +\item \texttt{eenough ({\ident} :\ {\form}) by {\tac}}\tacindex{eenough}\tacindex{eenough as}\tacindex{eenough by}\\ + \texttt{eenough {\form} by {\tac}}\tacindex{enough by}\\ + \texttt{eenough {\form} as {\intropattern} by {\tac}} + + While the different variants of \texttt{enough} expect that no + existential variables are generated by the tactic, \texttt{eenough} + removes this constraint. + \item {\tt cut {\form}}\tacindex{cut} This tactic applies to any goal. It implements the non-dependent From bbde815f8108f4641f5411d03f7a88096cc2221b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 24 May 2017 21:55:21 +0200 Subject: [PATCH 5/5] Support for using type information to infer more precise evar sources. This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted). --- engine/evarutil.ml | 4 ++-- engine/evarutil.mli | 2 +- engine/evd.ml | 3 ++- engine/evd.mli | 2 +- engine/proofview.ml | 6 ++++++ engine/termops.ml | 1 + interp/constrintern.ml | 12 ++++++------ intf/evar_kinds.mli | 2 +- plugins/ltac/extratactics.ml4 | 6 +++--- pretyping/cases.ml | 8 ++++---- pretyping/coercion.ml | 8 ++++---- pretyping/pretyping.ml | 16 ++++++++++++++++ tactics/hipattern.ml | 2 +- test-suite/.csdp.cache | Bin 89077 -> 89077 bytes test-suite/output/Show.out | 6 +++--- test-suite/output/inference.out | 10 +++++----- test-suite/output/inference.v | 2 +- test-suite/output/names.out | 6 ++++++ test-suite/output/names.v | 4 ++++ test-suite/success/Abstract.v | 1 - vernac/command.ml | 2 +- vernac/obligations.ml | 2 +- 22 files changed, 69 insertions(+), 36 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6cba6f6075c1..3ef725cbbd1d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -367,10 +367,10 @@ let push_rel_context_to_named_context env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let restrict_evar evd evk filter candidates = +let restrict_evar evd evk filter ?src candidates = let evd = Sigma.to_evar_map evd in let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in - let evd, evk' = Evd.restrict evk filter ?candidates evd in + let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) let new_pure_evar_full evd evi = diff --git a/engine/evarutil.mli b/engine/evarutil.mli index fcc435a2ecbd..496ec5bc4364 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -57,7 +57,7 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> - constr list option -> (existential_key, 'r) Sigma.sigma + ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma (** Polymorphic constants *) diff --git a/engine/evd.ml b/engine/evd.ml index b677705bc9c9..48fceae9ecb9 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -653,12 +653,13 @@ let define evk body evd = let evar_names = EvNames.remove_name_defined evk evd.evar_names in { evd with defn_evars; undf_evars; last_mods; evar_names } -let restrict evk filter ?candidates evd = +let restrict evk filter ?candidates ?src evd = let evk' = new_untyped_evar () in let evar_info = EvMap.find evk evd.undf_evars in let evar_info' = { evar_info with evar_filter = filter; evar_candidates = candidates; + evar_source = (match src with None -> evar_info.evar_source | Some src -> src); evar_extra = Store.empty } in let last_mods = match evd.conv_pbs with | [] -> evd.last_mods diff --git a/engine/evd.mli b/engine/evd.mli index 00533247066a..86755c360bc6 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -240,7 +240,7 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> (** {6 Misc} *) val restrict : evar -> Filter.t -> ?candidates:constr list -> - evar_map -> evar_map * evar + ?src:Evar_kinds.t located -> evar_map -> evar_map * evar (** Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates *) diff --git a/engine/proofview.ml b/engine/proofview.ml index ddfc0e39ddfa..29bb1ef39775 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -696,6 +696,12 @@ let mark_in_evm ~goal evd content = let info = if goal then { info with Evd.evar_source = match info.Evd.evar_source with + (* Two kinds for goal evars: + - GoalEvar (morally not dependent) + - VarInstance (morally dependent of some name). + This is a heuristic for naming these evars. *) + | loc, (Evar_kinds.QuestionMark (_,Names.Name id) | + Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x | loc,_ -> loc,Evar_kinds.GoalEvar } else info diff --git a/engine/termops.ml b/engine/termops.ml index ca32c06a7589..1ec2b81039cc 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -112,6 +112,7 @@ let pr_evar_suggested_name evk sigma = | None -> match evi.evar_source with | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id | _,Evar_kinds.VarInstance id -> id + | _,Evar_kinds.QuestionMark (_,Name id) -> id | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" | _ -> let env = reset_with_named_context evi.evar_hyps (Global.env()) in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4dcf287efcdc..6514ad8be5ef 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1081,8 +1081,8 @@ let sort_fields ~complete loc fields completer = let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc = match projs with | [] -> (idx, acc_first_idx, acc) - | (Some name) :: projs -> - let field_glob_ref = ConstRef name in + | (Some field_glob_id) :: projs -> + let field_glob_ref = ConstRef field_glob_id in let first_field = eq_gr field_glob_ref first_field_glob_ref in begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch") @@ -1099,7 +1099,7 @@ let sort_fields ~complete loc fields completer = build_proj_list projs proj_kinds idx ~acc_first_idx acc else build_proj_list projs proj_kinds (idx+1) ~acc_first_idx - ((idx, field_glob_ref) :: acc) + ((idx, field_glob_id) :: acc) end | None :: projs -> if complete then @@ -1121,7 +1121,7 @@ let sort_fields ~complete loc fields completer = user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern" (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in let remaining_projs, (field_index, _) = - let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in + let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in try CList.extract_first the_proj remaining_projs with Not_found -> user_err ?loc @@ -1646,7 +1646,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in let fields = sort_fields ~complete:true loc fs - (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st), + (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)), Misctypes.IntroAnonymous, None)) in begin @@ -1726,7 +1726,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in (match naming with | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id - | _ -> Evar_kinds.QuestionMark st) + | _ -> Evar_kinds.QuestionMark (st,Anonymous)) | Some k -> k in let solve = match solve with diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 470ad2a23b4b..835e94c777dc 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -21,7 +21,7 @@ type t = * bool (** Force inference *) | BinderType of Name.t | NamedHole of Id.t (* coming from some ?[id] syntax *) - | QuestionMark of obligation_definition_status + | QuestionMark of obligation_definition_status * Name.t | CasesType of bool (* true = a subterm of the type *) | InternalHole | TomatchTypeParameter of inductive * int diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index d68139a4b438..cba9c1364876 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -636,7 +636,7 @@ let subst_var_with_hole occ tid t = else (incr locref; CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true), + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), Misctypes.IntroAnonymous, None))) else x | c -> map_glob_constr_left_to_right substrec c in @@ -648,13 +648,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } -> + | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } -> decr occref; if Int.equal !occref 0 then tc else (incr locref; CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c2c8065a98ee..42615737255d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2064,8 +2064,8 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = CAst.make @@ - GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false), +let hole na = CAst.make @@ + GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = @@ -2168,7 +2168,7 @@ let vars_of_ctx sigma ctx = prev, (CAst.make @@ GApp ( (CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole; CAst.make @@ GVar prev])) :: vars + [hole na; CAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" @@ -2301,7 +2301,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = | l -> CAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> CAst.make @@ GApp (branch, [ hole ]) + Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ]) | None -> branch in incr i; diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3ef17912f794..83c26058aceb 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -90,8 +90,8 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 = open Program -let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) env evdref c = - let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in +let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = + let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in Evarutil.e_new_evar env evdref ~src c let app_opt env evdref f t = @@ -181,7 +181,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in - let evar = make_existential ?loc env evdref eq in + let evar = make_existential ?loc n env evdref eq in let eq_app x = papp evdref coq_eq_rect [| eqT; hdx; pred; x; hdy; evar|] in @@ -324,7 +324,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) Some (fun x -> let cx = app_opt env evdref c x in - let evar = make_existential ?loc env evdref (mkApp (p, [| cx |])) + let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |])) in (papp evdref sig_intro [| u; p; cx; evar |])) | None -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e72394fa283c..b0663af70c0e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -383,6 +383,21 @@ let process_inference_flags flags env initial_sigma (sigma,c) = let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c +let adjust_evar_source evdref na c = + match na, kind !evdref c with + | Name id, Evar (evk,args) -> + let evi = Evd.find !evdref evk in + begin match evi.evar_source with + | loc, Evar_kinds.QuestionMark (b,Anonymous) -> + let src = (loc,Evar_kinds.QuestionMark (b,na)) in + let sigma = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (evk', evd, _) = restrict_evar sigma evk (evar_filter evi) ~src None in + evdref := Sigma.to_evar_map evd; + mkEvar (evk',args) + | _ -> c + end + | _, _ -> c + (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false @@ -785,6 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre args, nf_evar !evdref (j_val hj) else [], j_val hj in + let ujval = adjust_evar_source evdref na ujval in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in let j = { uj_val = value; uj_type = typ } in apply_rec env (n+1) j candargs rest diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index fd5eabe6481d..35fbec5a6df0 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -254,7 +254,7 @@ open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) let mkGApp f args = CAst.make @@ GApp (f, args) let mkGHole = CAst.make @@ - GHole (QuestionMark (Define false), Misctypes.IntroAnonymous, None) + GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None) let mkGProd id c1 c2 = CAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) let mkGArrow c1 c2 = CAst.make @@ diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache index b99d80e95f06e77c5e2122b1c2e6a893c0600a77..ba85286dd3c0187ad1907ef8c039e67f40fede4e 100644 GIT binary patch delta 2221 zcmZuzeNa@_6`%9ozPDe%B8Ysriwl?qSztFX5={d#L_iI?iyx>k2}?8@g9weaHnpP0 z#F+&7aDRrYXzLm$^&_clyyBb0Dr%=TQ`0P|t+7d?cBW&S(JFOn)kLKCt-)qG{p0O@ z=e%>zJ@ll~W#u_gdJ&aw^7yT`wT;3nL~P7@wpX2|cFQ z#Z%6vIcY3x9y3}^F6=h0f!DYa7m_EiZUY%{GEGI5`7C_aKd`+rrQ_r-3-((MAlC9S z!WnLyG8y5MO#IoH6hd*_QLKqQjR)~z{HSO;PQ{mEs8C-s;kVs|-=Q*FB`K&MACJYh zR2Unkr7CrKuWS)G)LH&P0a zoZ=VfIYdA<^u?K2!3^>-e;rLiUrLuaJr}LaioP@xp7AE&r#r2~^U34X`*Ca&P*2 z!f8hf8XW=N=On^mXAq^%@AJc1R)UoEF0x|WA~+SVIVNLV=5>59@kMNQ?dKVfEg?8^ zZi#0py0SZQZm}0%6(r!to|(dbKCTwj@DuL)63p(SST54rmfOx^s>ptL9^2RsyQcCIlKz^5(`72~Epe(cGBN zcP>3I;mn&$*w!3RTUpuDWo3MDOQ*~av;`y#{oRa6a|2p8 z)!{F%-{u3a3T0rvOCaVD>lk#sG?uq+@)2h(@9O4>T;NH3!P>1d53K&T%y+c>M&`?! z3Jtt=ZNvZW{S2X9>3SqA-$^F!Z_g&UvvnSu5Zb;L!#y(vTK|+lU7H2F z_2P_0>libzERy;H-`pgB^>}oue~OMK?>L zGWK&HJsz!2Pwzs6c6jiUoo!;h7VOBt$d2{w%5+j$!(6g`yJra-P{oeRV-(!%J%TO0 zg*f4MAmlQ@GdGEccAu5tYS&xAd-&&`Ei62p-00rZ$k&GI34zr{*6yN-{L6QKE3 zl*fnn9+gp5tGAX4eBP0Z6Vu{w`JfX$<+GX7L0Q2YV|kl)K*I1H9Sd>aX{nC9B%S$>dbEW-m1<+AF#AF9i*&O`71$4OtU>xgw)l&SRlULHC*Md$cR% z^eM5D3fdytn+dD-WJbx{mlnr1R*002Os7(Oknk|!gOOMrpHvLSTSwCyMJx};0&d-@ znUz)1X1zo0(EYJ~pO8l8(BU2*dEqRIa^&sNmq%pT&b&TK9HovG;g<{;s1XHeGqUGq zQ`NCqbXU@TRYfI|j-Hdz+&JAC=}jZNWm4NVNZGLtd%FVPd7V)W$wsKxHDI^CQ^iT*pT1e@5(6s`?**cc5BL(~AeSD5)9q}YZN4WRc z#)g6@6d`A_r~sMz&G_>oCx(l32rkyQTgbo~-NHPaWMF42$OvzgjCj2jN|XzAx++{8 zAA{P4U}o2m7Nv$yVfeib7lNwT>spG&i19c~#=l}^yaTQ%1!a-}*Gf{bBls2@{uwz? zX>NxaVZ%VW3EifhXvmm}0^0;Mho)jUqZEyyQEis{Xtad2S)%Z7^8k*;I&n301ZFl~ zSY_5!L=&*2PY2&wu}%BL=Rm${+;RyIGShj%gv%s?Ex;=g^I(l|V|bTMglELH2oo%k zQ`kcfO+|miCoHj&(wJ{1g(H7bFa~XA)>=hjxIHP74OG%k*qS0T3)5z#O$_^SvtF2r zuq&!bROu}kZPhql;*U*+Hzp6)qP@J{wuN}VT_W_`_aV>T$XCW!5I%`Jj3XlR))74# ztMzTIMx1R4XFa8)_zSEmkXHn4Dp`ajh0&AQ}GX9Yng>N#> zVX#<>fsC!A|IwI}F^NCO)Jy#KPruS&?~%Fa`pm{%Gfr!{Gp9p?<$VDJt{IbgOIDYJ zKNNL{D%SDE#S0`JI{PmYZgv|)YT@{{%*!+{k&_$e2()3|Z}_9~)r6PJ4{&out`;Bm z#^8cphb3udG_TjfE9+n>j%Il>>9})Y4qE@yzE@CMJC6Ben!>IZi}7)k z&=gUAJ=;=D@uT*)`P%vs32W<}+_2(H@v_{@?HlVP)KyO9_MI~ESKrLg@{4o$>QXOO7!f*Vw#2-ReBuk3NV3*yLTlJZnrNIzgS!e6I0eP z33*H})-KrNjd^}X!pmB@|BSxOFFx&s+_tMdk? zK4AvdTS!@gJJ;}@0}mxOtw?O@4s~I$+kyo>v20+b;IF;iHGD%)4KY{V6UsI6NALG( zSWYgb_!-!UNAIUI(~F|j@(+pH?|3(vtt+C00Aqd7yMnt<{!N3FoVm;wF4|-8WFh}; z)=LsQT_L9Z)QNUjzjBCF45-VA47eOWs%rU)K8J=+J!O#D3z7&T=t4Q}mqp;(#jD(R zehu;7FQ#eumUB)GetB*ik3Q;^P;xGd-x^$@!AD^>^bbxKGo1zRU@=QmNEB+Y41H&( z!PFNejG^t7g3Qx0gW&6wG0(Y({d@7%CTB69~HzLYP) zaySg19j#vPlEl^SUkz8fdlyW9d(Oaff#T6L+Oyu@mB)QS4?JOMj! zt1}pNNx^3_lrP_%o1$4 zT4EGJ*(}>FDt|#AGN#fIxZ?3ku8!S~rIQkQSZE=osN3ySKx$eZ`829%%X=EN=mq+( ztX@f_)v|gjk?e~4UL08!oYJPir!&F5YrpC%q)Q}5!#_wSf6G?km1hep8<|PjLMx)! z^}t-%g#3icej*tw<|Hf?+HlrQft3S-88Imek z{Jz8dDVbd_rOB+^Z*$HL*rLRpMqwePw9$_o@qe;qbe7}9 zT*fg=3FWKX-Slh1ga|uZ=q49Ss1y$&?uy`skg=K;>3`|fzHa~k diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out index bf1bf2809d2d..8acfed5d00f3 100644 --- a/test-suite/output/Show.out +++ b/test-suite/output/Show.out @@ -1,12 +1,12 @@ -3 subgoals (ID 29) +3 subgoals (ID 31) H : 0 = 0 ============================ 1 = 1 -subgoal 2 (ID 33) is: +subgoal 2 (ID 35) is: 1 = S (S m') -subgoal 3 (ID 20) is: +subgoal 3 (ID 22) is: S (S n') = S m (dependent evars: (printing disabled) ) diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index c70467912fbf..d28ee427615e 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,13 +6,13 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x : T n := A n in ?t ?y : T n +fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where -?t : [n : nat x := A n : T n |- ?T -> T n] -?y : [n : nat x := A n : T n |- ?T] -fun n : nat => ?t ?y : T n +?t : [n : nat y := A n : T n |- ?T -> T n] +?x : [n : nat y := A n : T n |- ?T] +fun n : nat => ?t ?x : T n : forall n : nat, T n where ?t : [n : nat |- ?T -> T n] -?y : [n : nat |- ?T] +?x : [n : nat |- ?T] diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 1825db1676b6..f761a4dc5a63 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). (* Note: exact numbers of evars are not important... *) Inductive T (n:nat) : Type := A : T n. -Check fun n (x:=A n:T n) => _ _ : T n. +Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/output/names.out b/test-suite/output/names.out index 9471b892ddd1..48be63a46ab8 100644 --- a/test-suite/output/names.out +++ b/test-suite/output/names.out @@ -3,3 +3,9 @@ In environment y : nat The term "a y" has type "{y0 : nat | y = y0}" while it is expected to have type "{x : nat | x = y}". +1 focused subgoal +(shelved: 1) + + H : ?n <= 3 -> 3 <= ?n -> ?n = 3 + ============================ + True diff --git a/test-suite/output/names.v b/test-suite/output/names.v index b3b5071a032d..f1efd0df2aca 100644 --- a/test-suite/output/names.v +++ b/test-suite/output/names.v @@ -3,3 +3,7 @@ Parameter a : forall x, {y:nat|x=y}. Fail Definition b y : {x:nat|x=y} := a y. + +Goal (forall n m, n <= m -> m <= n -> n = m) -> True. +intro H; epose proof (H _ 3) as H. +Show. diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index ffd50f6efd4a..69dc9aca7823 100644 --- a/test-suite/success/Abstract.v +++ b/test-suite/success/Abstract.v @@ -1,4 +1,3 @@ - (* Cf coqbugs #546 *) Require Import Omega. diff --git a/vernac/command.ml b/vernac/command.ml index e2ebb4d7fb4b..25dd724af805 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1062,7 +1062,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)), [| argtyp ; wf_rel ; Evarutil.e_new_evar env evdref - ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; + ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof; prop |]) in let def = Typing.e_solve_evars env evdref def in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index be58c67a9e3d..47ac16f9c7b8 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -221,7 +221,7 @@ let eterm_obligations env name evm fs ?status t ty = in let loc, k = evar_source id evm in let status = match k with - | Evar_kinds.QuestionMark o -> o + | Evar_kinds.QuestionMark (o,_) -> o | _ -> match status with | Some o -> o | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))