diff options
33 files changed, 214 insertions, 85 deletions
@@ -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 fc3fdd002..def42955f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1155,6 +1155,15 @@ Section~\ref{Occurrences_clauses}. 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 @@ Section~\ref{Occurrences_clauses}. 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 @@ Section~\ref{Occurrences_clauses}. 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 @@ in the list of subgoals remaining to prove. \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 @@ in the list of subgoals remaining to prove. 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 @@ in the list of subgoals remaining to prove. 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 diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6cba6f607..3ef725cbb 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 fcc435a2e..496ec5bc4 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 b677705bc..48fceae9e 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 005332470..86755c360 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 ddfc0e39d..29bb1ef39 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 ca32c06a7..1ec2b8103 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 4dcf287ef..6514ad8be 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 470ad2a23..835e94c77 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 d68139a4b..cba9c1364 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/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 1404b1c1f..83bfd0233 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -538,38 +538,64 @@ 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; ":="; 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 a001c6a2b..4e254ea76 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 -> @@ -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 bf760e7bb..b78dc3742 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -141,10 +141,10 @@ 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 * + | 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 e431a13bc..2dc3bb378 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -489,17 +489,17 @@ 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 -> 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 a9ec779d1..6b0914ff9 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 -> @@ -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 4390ff08b..f5e6f05ce 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -146,13 +146,13 @@ 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) - | 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/pretyping/cases.ml b/pretyping/cases.ml index c2c8065a9..426157372 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 3ef17912f..83c26058a 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 e72394fa2..b0663af70 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 fd5eabe64..35fbec5a6 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/tactics/tactics.ml b/tactics/tactics.ml index 7e8cb4e63..f4408d403 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 07a803542..0dbcce02c 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. } *) diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b99d80e95..ba85286dd 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out index bf1bf2809..8acfed5d0 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 c70467912..d28ee4276 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 1825db167..f761a4dc5 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 9471b892d..48be63a46 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 b3b5071a0..f1efd0df2 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 ffd50f6ef..69dc9aca7 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/test-suite/success/forward.v b/test-suite/success/forward.v new file mode 100644 index 000000000..0ed5b524f --- /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. diff --git a/vernac/command.ml b/vernac/command.ml index e2ebb4d7f..25dd724af 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 be58c67a9..47ac16f9c 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 ())) |