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(-)

(limited to 'tactics')

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


From 08fa634493b8635a77174bbdcd0e1529e3c40279 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Nov 2015 18:43:50 +0100
Subject: Fix bug #4404: [remember] gives Error: Conversion test raised an
 anomaly.

---
 tactics/tactics.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 37b715ebe2..0a013e95f7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2345,7 +2345,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
-    let t = match ty with Some t -> t | _ -> typ_of env sigma c in
+    let (sigma, t) = match ty with
+    | Some t -> (sigma, t)
+    | None ->
+      let t = typ_of env sigma c in
+      Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t
+    in
     let eq_tac gl = match with_eq with
       | Some (lr,(loc,ido)) ->
           let heq = match ido with
-- 
cgit v1.2.3


From 1b163c6230ecd78526bb404fb2b7cc04985df2d9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2015 17:29:28 +0200
Subject: Typo.

---
 tactics/ftactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index fea0432aea..a688b94879 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -16,7 +16,7 @@ type 'a focus =
 
 (** Type of tactics potentially goal-dependent. If it contains a [Depends],
     then the length of the inner list is guaranteed to be the number of
-    currently focussed goals. Otherwise it means the tactic does not depends
+    currently focussed goals. Otherwise it means the tactic does not depend
     on the current set of focussed goals. *)
 type 'a t = 'a focus Proofview.tactic
 
-- 
cgit v1.2.3