diff --git a/doc/changelog/04-tactics/18395-master+use-intro-name-in-evar-context-when-goal-is-evar.rst b/doc/changelog/04-tactics/18395-master+use-intro-name-in-evar-context-when-goal-is-evar.rst new file mode 100644 index 000000000000..62bc5bf97824 --- /dev/null +++ b/doc/changelog/04-tactics/18395-master+use-intro-name-in-evar-context-when-goal-is-evar.rst @@ -0,0 +1,10 @@ +- **Changed:** + Tactic :g:`intro z` on an existential variable goal forces the resolution + of the existential variable into a goal :g:`forall z:?T, ?P`, which + becomes :g:`?P` in context :g:`z:?T` after introduction. The + existential variable :n:`?P` itself is now defined in a context + where the variable of type `?T` is also named :g:`z`, as specified + by :tacn:`intro` instead of :g:`x` as it was conventionally the case + before + (`#18395 `_, + by Hugo Herbelin). diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 99099260c6ad..80c0b4e2f2f2 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -71,11 +71,12 @@ let idx = Namegen.default_dependent_ident (* Refining an evar to a product *) -let define_pure_evar_as_product env evd evk = +let define_pure_evar_as_product env evd na evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env env evi in - let id = next_ident_away idx (Environ.ids_of_named_context_val (Evd.evar_hyps evi)) in + let id = match na with Some id -> id | None -> idx in + let id = next_ident_away id (Environ.ids_of_named_context_val (Evd.evar_hyps evi)) in let concl = Reductionops.whd_all evenv evd (Evd.evar_concl evi) in let s = destSort evd concl in let evksrc = evar_source evi in @@ -106,8 +107,8 @@ let define_pure_evar_as_product env evd evk = (* Refine an applied evar to a product and returns its instantiation *) -let define_evar_as_product env evd (evk,args) = - let evd,prod = define_pure_evar_as_product env evd evk in +let define_evar_as_product env evd ?name (evk,args) = + let evd,prod = define_pure_evar_as_product env evd name evk in (* Quick way to compute the instantiation of evk with args *) let na,dom,rng = destProd evd prod in let evdom = mkEvar (fst (destEvar evd dom), args) in @@ -124,14 +125,14 @@ let define_evar_as_product env evd (evk,args) = - x1..xq,y:A |- ?e':B *) -let define_pure_evar_as_lambda env evd evk = +let define_pure_evar_as_lambda env evd name evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env env evi in let typ = Reductionops.whd_all evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match EConstr.kind evd typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) - | Evar ev' -> let evd,typ = define_evar_as_product env evd ev' in evd,destProd evd typ + | Evar ev' -> let evd,typ = define_evar_as_product env evd ?name ev' in evd,destProd evd typ | _ -> error_not_product env evd typ in let avoid = Environ.ids_of_named_context_val (Evd.evar_hyps evi) in let id = @@ -146,8 +147,8 @@ let define_pure_evar_as_lambda env evd evk = let lam = mkLambda (map_annot Name.mk_name id, dom, subst_var evd2 id.binder_name body) in Evd.define evk lam evd2, lam -let define_evar_as_lambda env evd (evk,args) = - let evd,lam = define_pure_evar_as_lambda env evd evk in +let define_evar_as_lambda env evd ?name (evk,args) = + let evd,lam = define_pure_evar_as_lambda env evd name evk in (* Quick way to compute the instantiation of evk with args *) let na,dom,body = destLambda evd lam in let evbodyargs = SList.cons (mkRel 1) (SList.Skip.map (lift 1) args) in @@ -158,7 +159,7 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function | [] -> evd,ev | a::l -> (* TODO: optimize and avoid introducing intermediate evars *) - let evd,lam = define_pure_evar_as_lambda env evd evk in + let evd,lam = define_pure_evar_as_lambda env evd None evk in let _,_,body = destLambda evd lam in let evk = fst (destEvar evd body) in evar_absorb_arguments env evd (evk, SList.cons a args) l diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index b4ecfe8f933d..3f67cb1cc7c6 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -38,8 +38,8 @@ val split_as_array : env -> evar_map -> type_constraint -> val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : int -> type_constraint -> type_constraint -val define_evar_as_product : env -> evar_map -> existential -> evar_map * types -val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types +val define_evar_as_product : env -> evar_map -> ?name:Names.Id.t -> existential -> evar_map * types +val define_evar_as_lambda : env -> evar_map -> ?name:Names.Id.t -> existential -> evar_map * types val define_evar_as_sort : env -> evar_map -> existential -> evar_map * ESorts.t (** {6 debug pretty-printer:} *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 051bf3e3d8ae..7893e9555547 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1077,7 +1077,8 @@ let rec intro_then_gen name_flag move_flag ~force ~dep tac = let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | Evar ev when force -> - let sigma, t = Evardefine.define_evar_as_product env sigma ev in + let name = find_name false (LocalAssum (anonR,concl)) name_flag gl in + let sigma, t = Evardefine.define_evar_as_product env sigma ~name ev in Tacticals.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (intro_then_gen name_flag move_flag ~force ~dep tac) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 81f5a110ceae..58fe620f866b 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -133,9 +133,9 @@ Module Evar. Goal exists (A:Prop), A. eexists. -unshelve (intro x). +unshelve (intro y). - exact nat. -- exact (x=x). +- exact (y=y). - auto. Qed.