From 64637ffc5054199459d9fc7f07b84a99da71c6f1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 17:24:05 +0100
Subject: Removing "intro" from the tactic AST.

Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.
---
 theories/MSets/MSetAVL.v       | 1 +
 theories/Reals/Ranalysis_reg.v | 9 +++++++++
 2 files changed, 10 insertions(+)

(limited to 'theories')

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index cc023cc3f8..a3c265a21f 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -417,6 +417,7 @@ Local Open Scope Int_scope.
     Let's do its job by hand: *)
 
 Ltac join_tac :=
+ let l := fresh "l" in
  intro l; induction l as [| lh ll _ lx lr Hlr];
    [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join;
      [ | destruct ((rh+2) <? lh) eqn:LT;
diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v
index e57af7311f..0c27d407c3 100644
--- a/theories/Reals/Ranalysis_reg.v
+++ b/theories/Reals/Ranalysis_reg.v
@@ -109,6 +109,7 @@ Ltac intro_hyp_glob trm :=
     | Rabs => idtac
     | ?X1 =>
       let p := constr:(X1) in
+      let HYPPD := fresh "HYPPD" in
         match goal with
           | _:(derivable p) |- _ => idtac
           |  |- (derivable p) => idtac
@@ -250,6 +251,7 @@ Ltac intro_hyp_pt trm pt :=
       end
     | ?X1 =>
       let p := constr:(X1) in
+      let HYPPD := fresh "HYPPD" in
         match goal with
           | _:(derivable_pt p pt) |- _ => idtac
           |  |- (derivable_pt p pt) => idtac
@@ -341,8 +343,10 @@ Ltac is_diff_pt :=
     | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) =>
       assumption
     | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ]
     |  |- (True -> derivable_pt _ _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_diff_pt
     | _ =>
       try
@@ -411,6 +415,7 @@ Ltac is_diff_glob :=
       apply (derivable_comp X2 X1); is_diff_glob
     | _:(derivable ?X1) |- (derivable ?X1) => assumption
     |  |- (True -> derivable _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_diff_glob
     | _ =>
       try
@@ -490,14 +495,17 @@ Ltac is_cont_pt :=
     | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
       assumption
     | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ]
     | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
       apply derivable_continuous_pt; assumption
     | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (continuity X1);
         [ intro HypDDPT; apply HypDDPT
           | apply derivable_continuous; assumption ]
     |  |- (True -> continuity_pt _ _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_cont_pt
     | _ =>
       try
@@ -567,6 +575,7 @@ Ltac is_cont_glob :=
       apply (continuity_comp X2 X1); try is_cont_glob || assumption
     | _:(continuity ?X1) |- (continuity ?X1) => assumption
     |  |- (True -> continuity _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_cont_glob
     | _:(derivable ?X1) |- (continuity ?X1) =>
       apply derivable_continuous; assumption
-- 
cgit v1.2.3