From e6a054695a2f5d8be3f695975464f99571a69b75 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Sep 2016 19:20:23 +0200 Subject: Ensuring that the evar name is preserved by "rename" as it is already the case for clear and the conversion tactics. --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a66dbd6e88..225ff3db94 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -335,7 +335,7 @@ let rename_hyp repl = let nctx = Environ.val_of_named_context nhyps in let instance = List.map (fun (id, _, _) -> mkVar id) hyps in Proofview.Refine.refine ~unsafe:true begin fun sigma -> - Evarutil.new_evar_instance nctx sigma nconcl ~store instance + Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance end end -- cgit v1.2.3