Removing "intros untils" from the AST.

5 files changed, 11 insertions, 11 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index a07069bd37..d49040fc02 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -139,3 +139,9 @@ TACTIC EXTEND esplit_with
     Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true) sigma [bl]
   ]
 END
+
+(** Intro *)
+
+TACTIC EXTEND intros_until
+  [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
+END
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 0697ae5529..2937d42731 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -246,7 +246,9 @@ let coerce_to_quantified_hypothesis v =
     NamedHyp id
   else if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
-  else raise (CannotCoerceTo "a quantified hypothesis")
+  else match Value.to_constr v with
+  | Some c when isVar c -> NamedHyp (destVar c)
+  | _ -> raise (CannotCoerceTo "a quantified hypothesis")
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
@@ -255,9 +257,7 @@ let coerce_to_decl_or_quant_hyp env v =
   if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else
-    try
-      let hyp = coerce_to_hyp env v in
-      NamedHyp hyp
+    try coerce_to_quantified_hypothesis v
     with CannotCoerceTo _ ->
       raise (CannotCoerceTo "a declared or quantified hypothesis")
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 80711cf815..60bc784f1f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -456,7 +456,6 @@ let rec intern_atomic lf ist x =
   (* Basic tactics *)
   | TacIntroPattern l ->
       TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
-  | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,hto) ->
       TacIntroMove (Option.map (intern_ident lf ist) ido,
                     intern_move_location ist hto)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0432b08ec5..95752c99a8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1532,11 +1532,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let patterns = interp_intro_pattern_list_as_list ist env l in
         Tactics.intro_patterns patterns
       end
-  | TacIntrosUntil hyp ->
-      begin try (* interp_quantified_hypothesis can raise an exception *)
-        Tactics.intros_until (interp_quantified_hypothesis ist hyp)
-      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-      end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 0ff4fe9b8a..4bf2e5fb83 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -135,7 +135,7 @@ let rec subst_match_goal_hyps subst = function
 
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
-  | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
+  | TacIntroPattern _ | 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)