From eec77191b33bbca4c9d8b1b92b0c622ef430a3a8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 1 Nov 2015 11:20:34 +0100
Subject: Preservation of the name of evars/goals when applying
 pose/set/intro/clearbody.

For pose/set/clearbody, I think it is clear that we want to preserve
the name and this commit do it.

For revert, I first did not preserve the name, then considered in
2ba2ca96be88 that it was better to preserve it.

For intro, like for revert actually, I did not preserve the name,
based on the idea that the type was changing (*). For instance if we have
?f:nat->nat, do we really want to keep the name f in ?f:nat after an
intro.

For revert, I changed my mind based on the idea that if we had a
better control of the name if we keep the name that if the system
invents a new one based on the type. I think this is more reasonable
than (*), so this commit preserves the name for intro.

For generalize, it is still not done because of generalize being in
the old proof engine.
---
 tactics/tactics.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e215ff42f9..37b715ebe2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -164,7 +164,7 @@ let unsafe_intro env store (id, c, t) b =
     let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar id) b in
-    let sigma, ev = new_evar_instance nctx sigma nb ~store ninst in
+    let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
     sigma, mkNamedLambda_or_LetIn (id, c, t) ev
   end
 
@@ -1834,7 +1834,7 @@ let clear_body ids =
     in
     check_hyps <*> check_concl <*>
     Proofview.Refine.refine ~unsafe:true begin fun sigma ->
-      Evarutil.new_evar env sigma concl
+      Evarutil.new_evar env sigma ~principal:true concl
     end
   end
 
@@ -2599,7 +2599,7 @@ let new_generalize_gen_let lconstr =
     in
       Proofview.Unsafe.tclEVARS sigma <*>
 	Proofview.Refine.refine begin fun sigma ->
-          let (sigma, ev) = Evarutil.new_evar env sigma newcl in
+          let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in
             (sigma, (applist (ev, args)))
 	end
   end
-- 
cgit v1.2.3