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.

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e215ff42f..37b715ebe 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