Remove a few tactics from the Tacexpr AST.

Note that this breaks a few badly written scripts using intro in strict
mode without providing an existing identifier.

15 files changed, 76 insertions, 108 deletions

diff --git a/CHANGES b/CHANGES
index 9c89cdb8e5..41d61ec459 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,9 @@ Tactics
 - Every generic argument type declares a tactic scope of the form "name:(...)"
   where name is the name of the argument. This generalizes the constr: and ltac:
   instances.
+- When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use
+  a locally free identifier anymore. It must use e.g. the "fresh" primitive
+  instead (potential source of incompatibilities).
 
 Program
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e06436d8a3..379dd59d39 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -139,8 +139,6 @@ type intro_pattern_naming = intro_pattern_naming_expr located
 type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of 'dtrm intro_pattern_expr located list
-  | TacIntroMove of Id.t option * 'nam move_location
-  | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
       ('nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
@@ -157,10 +155,6 @@ type 'a gen_atomic_tactic_expr =
   (* Derived basic tactics *)
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
-  | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
-
-  (* Context management *)
-  | TacRename of ('nam *'nam) list
 
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index ce28eacc09..9879cfc280 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -26,6 +26,10 @@ TACTIC EXTEND reflexivity
   [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
 END
 
+TACTIC EXTEND exact
+  [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
+END
+
 TACTIC EXTEND assumption
   [ "assumption" ] -> [ Tactics.assumption ]
 END
@@ -197,6 +201,19 @@ TACTIC EXTEND intros_until
   [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
 END
 
+TACTIC EXTEND intro
+| [ "intro" ] -> [ Tactics.intro_move None MoveLast ]
+| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ]
+| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ]
+| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ]
+| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ]
+| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ]
+| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ]
+| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ]
+| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ]
+| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ]
+END
+
 (** Move *)
 
 TACTIC EXTEND move
@@ -206,6 +223,12 @@ TACTIC EXTEND move
 | [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
 END
 
+(** Rename *)
+
+TACTIC EXTEND rename
+| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ]
+END
+
 (** Revert *)
 
 TACTIC EXTEND revert
@@ -222,6 +245,13 @@ TACTIC EXTEND simple_destruct
   [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ]
 END
 
+(** Double induction *)
+
+TACTIC EXTEND double_induction
+  [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
+  [ Elim.h_double_induction h1 h2 ]
+END
+
 (* Admit *)
 
 TACTIC EXTEND admit
@@ -280,7 +310,6 @@ let initial_atomic () =
         "hnf", TacReduce(Hnf,nocl);
         "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl);
         "compute", TacReduce(Cbv Redops.all_flags,nocl);
-        "intro", TacIntroMove(None,MoveLast);
         "intros", TacIntroPattern [];
       ]
   in
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 0bddcc9fdd..e6d0a9c69c 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -15,6 +15,7 @@ open Constrarg
 open Pcoq.Prim
 open Pcoq.Constr
 open Names
+open Tacmach
 open Tacexpr
 open Taccoerce
 open Tacinterp
@@ -175,6 +176,16 @@ ARGUMENT EXTEND lglob
   [ lconstr(c) ] -> [ c ]
 END
 
+let interp_casted_constr ist gl c =
+  interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
+
+ARGUMENT EXTEND casted_constr
+  TYPED AS constr
+  PRINTED BY pr_gen
+  INTERPRETED BY interp_casted_constr
+  [ constr(c) ] -> [ c ]
+END
+
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
 type loc_place = Id.t Loc.located gen_place
@@ -225,6 +236,14 @@ ARGUMENT EXTEND hloc
 
  END
 
+let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m
+
+ARGUMENT EXTEND rename
+  TYPED AS ident * ident
+  PRINTED BY pr_rename
+| [ ident(n) "into" ident(m) ] -> [ (n, m) ]
+END
+
 (* Julien: Mise en commun des differentes version de replace with in by *)
 
 let pr_by_arg_tac _prc _prlc prtac opt_c =
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli
index 4d1d8ba7fe..0cf77935c2 100644
--- a/ltac/extraargs.mli
+++ b/ltac/extraargs.mli
@@ -16,6 +16,8 @@ val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
 val pr_orient : bool -> Pp.std_ppcmds
 
+val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
+
 val occurrences : (int list or_var) Pcoq.Gram.entry
 val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
 val pr_occurrences : int list or_var -> Pp.std_ppcmds
@@ -38,6 +40,11 @@ val wit_lconstr :
   Tacexpr.glob_constr_and_expr,
   Constr.t) Genarg.genarg_type
 
+val wit_casted_constr :
+  (constr_expr,
+  Tacexpr.glob_constr_and_expr,
+  Constr.t) Genarg.genarg_type
+
 val glob : constr_expr Pcoq.Gram.entry
 val lglob : constr_expr Pcoq.Gram.entry
 
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 3744449e97..d39f835528 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -481,10 +481,6 @@ let rec intern_atomic lf ist x =
   (* Basic tactics *)
   | TacIntroPattern l ->
       TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
-  | TacIntroMove (ido,hto) ->
-      TacIntroMove (Option.map (intern_ident lf ist) ido,
-                    intern_move_location ist hto)
-  | TacExact c -> TacExact (intern_constr ist c)
   | TacApply (a,ev,cb,inhyp) ->
       TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
                 Option.map (intern_in_hyp_as ist lf) inhyp)
@@ -520,16 +516,6 @@ let rec intern_atomic lf ist x =
                Option.map (intern_or_and_intro_pattern_loc lf ist) ipats),
                Option.map (clause_app (intern_hyp_location ist)) cls)) l,
                Option.map (intern_constr_with_bindings ist) el))
-  | TacDoubleInduction (h1,h2) ->
-      let h1 = intern_quantified_hypothesis ist h1 in
-      let h2 = intern_quantified_hypothesis ist h2 in
-      TacDoubleInduction (h1,h2)
-  (* Context management *)
-  | TacRename l ->
-      TacRename (List.map (fun (id1,id2) ->
-			     intern_hyp ist id1,
-			     intern_hyp ist id2) l)
-
   (* Conversion *)
   | TacReduce (r,cl) ->
       dump_glob_red_expr r;
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index fcc29a8302..5ee9b0fc4d 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -684,10 +684,6 @@ let interp_typed_pattern ist env sigma (_,c,_) =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
   pattern_of_constr env sigma c
 
-(* Interprets a constr expression casted by the current goal *)
-let pf_interp_casted_constr ist gl c =
-  interp_constr_gen (OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
-
 (* Interprets a constr expression *)
 let pf_interp_constr ist gl =
   interp_constr ist (pf_env gl) (project gl)
@@ -1644,24 +1640,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
              expected behaviour. *)
           (Tactics.intro_patterns l')) sigma
       end }
-  | TacIntroMove (ido,hto) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let mloc = interp_move_location ist env sigma hto in
-        let ido = Option.map (interp_ident ist env sigma) ido in
-        name_atomic ~env
-          (TacIntroMove(ido,mloc))
-          (Tactics.intro_move ido mloc)
-      end }
-  | TacExact c ->
-      (* spiwack: until the tactic is in the monad *)
-      Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
-      Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
-        let (sigma, c_interp) = pf_interp_casted_constr ist gl c in
-        Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma)
-      end }
-      end
   | TacApply (a,ev,cb,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
@@ -1822,26 +1800,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
-  | TacDoubleInduction (h1,h2) ->
-      let h1 = interp_quantified_hypothesis ist h1 in
-      let h2 = interp_quantified_hypothesis ist h2 in
-      name_atomic
-        (TacDoubleInduction (h1,h2))
-        (Elim.h_double_induction h1 h2)
-  (* Context management *)
-  | TacRename l ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = pf_env gl in
-        let sigma = project gl in
-        let l =
-          List.map (fun (id1,id2) ->
-	    interp_hyp ist env sigma id1,
-	    interp_ident ist env sigma (snd id2)) l
-        in
-        name_atomic ~env
-          (TacRename l)
-          (Tactics.rename_hyp l)
-      end }
 
   (* Conversion *)
   | TacReduce (r,cl) ->
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli
index 8bb6ee4cdf..6f64981eff 100644
--- a/ltac/tacinterp.mli
+++ b/ltac/tacinterp.mli
@@ -72,6 +72,9 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map
 val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
   Id.t Loc.located -> Id.t
 
+val interp_constr_gen : Pretyping.typing_constraint -> interp_sign ->
+  Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr
+
 val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
  glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
 
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 3f504b7f37..2c3c76ef74 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -137,8 +137,6 @@ let rec subst_match_goal_hyps subst = function
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
   | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l)
-  | TacIntroMove _ as x -> x
-  | TacExact c -> TacExact (subst_glob_constr subst c)
   | TacApply (a,ev,cb,cl) ->
       TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
   | TacElim (ev,cb,cbo) ->
@@ -162,10 +160,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
         subst_induction_arg subst c, ids, cls) l in
       let el' = Option.map (subst_glob_with_bindings subst) el in
       TacInductionDestruct (isrec,ev,(l',el'))
-  | TacDoubleInduction (h1,h2) as x -> x
-
-  (* Context management *)
-  | TacRename l as x -> x
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index cfe5377d63..36fffd74fa 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -528,13 +528,6 @@ GEXTEND Gram
           TacAtom (!@loc, TacIntroPattern pl)
       | IDENT "intros" ->
           TacAtom (!@loc, TacIntroPattern [!@loc,IntroForthcoming false])
-      | IDENT "intro"; id = ident; hto = move_location ->
-	  TacAtom (!@loc, TacIntroMove (Some id, hto))
-      | IDENT "intro"; hto = move_location -> TacAtom (!@loc, TacIntroMove (None, hto))
-      | IDENT "intro"; id = ident -> TacAtom (!@loc, TacIntroMove (Some id, MoveLast))
-      | IDENT "intro" -> TacAtom (!@loc, TacIntroMove (None, MoveLast))
-
-      | IDENT "exact"; c = constr -> TacAtom (!@loc, TacExact c)
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
@@ -606,16 +599,11 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct (true,false,ic))
       | IDENT "einduction"; ic = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(true,true,ic))
-      | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
-	  h2 = quantified_hypothesis -> TacAtom (!@loc, TacDoubleInduction (h1,h2))
       | IDENT "destruct"; icl = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(false,false,icl))
       | IDENT "edestruct";  icl = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
-      (* Context management *)
-      | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
-
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
 	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 36511386ac..5e43dfc42d 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1074,16 +1074,19 @@ Qed.
    avait utilisé le test précédent et fait une elimination dessus. *)
 
 Ltac elim_eq_term t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (eq_term_true t1 t2 Aux); clear Aux
    | generalize (eq_term_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_beq t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (beq t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (beq_true t1 t2 Aux); clear Aux
    | generalize (beq_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_bgt t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (bgt t1 t2); apply bool_eq_ind; intro Aux;
   [ generalize (bgt_true t1 t2 Aux); clear Aux
   | generalize (bgt_false t1 t2 Aux); clear Aux ].
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 44c832bd7a..114410fed1 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -816,7 +816,6 @@ module Make
       (* Printing tactics as arguments *)
       let rec pr_atom0 a = tag_atom a (match a with
         | TacIntroPattern [] -> primitive "intros"
-        | TacIntroMove (None,MoveLast) -> primitive "intro"
         | t -> str "(" ++ pr_atom1 t ++ str ")"
       )
 
@@ -828,15 +827,6 @@ module Make
         | TacIntroPattern (_::_ as p) ->
           hov 1 (primitive "intros" ++ spc () ++
                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
-        | TacIntroMove (None,MoveLast) as t ->
-          pr_atom0 t
-        | TacIntroMove (Some id,MoveLast) ->
-          primitive "intro" ++ spc () ++ pr_id id
-        | TacIntroMove (ido,hto) ->
-          hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
-                    Miscprint.pr_move_location pr.pr_name hto)
-        | TacExact c ->
-          hov 1 (primitive "exact" ++ pr_constrarg c)
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
             (if a then mt() else primitive "simple ") ++
@@ -909,23 +899,6 @@ module Make
                 pr_opt (pr_clauses None pr.pr_name) cl) l ++
               pr_opt pr_eliminator el
           )
-        | TacDoubleInduction (h1,h2) ->
-          hov 1 (
-            primitive "double induction"
-            ++ pr_arg pr_quantified_hypothesis h1
-            ++ pr_arg pr_quantified_hypothesis h2
-          )
-
-        (* Context management *)
-        | TacRename l ->
-          hov 1 (
-            primitive "rename" ++ brk (1,1)
-            ++ prlist_with_sep
-              (fun () -> str "," ++ brk (1,1))
-              (fun (i1,i2) ->
-                pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
-              l
-          )
 
         (* Conversion *)
         | TacReduce (r,h) ->
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc60897d21..fc4c171e2c 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,6 +2,7 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "coretactics".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
 Delimit Scope type_scope with type.
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