Removing "intros untils" from the AST.

9 files changed, 12 insertions, 19 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 4fede761f..1614301ec 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -303,8 +303,6 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacIntroPattern pl ->
       let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in
       <:expr< Tacexpr.TacIntroPattern $pl$ >>
-  | Tacexpr.TacIntrosUntil h ->
-      <:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacIntroMove (idopt,idopt') ->
       let idopt = mlexpr_of_ident_option idopt in
       let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 0c5eed714..7f7ecdcf7 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -111,7 +111,6 @@ type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of intro_pattern_expr located list
-  | TacIntrosUntil of quantified_hypothesis
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3c097db1c..29cb45ad1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -528,9 +528,7 @@ GEXTEND Gram
   simple_tactic:
     [ [
       (* Basic tactics *)
-        IDENT "intros"; IDENT "until"; id = quantified_hypothesis ->
-	  TacIntrosUntil id
-      | IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
+        IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
       | IDENT "intro"; id = ident; hto = move_location ->
 	  TacIntroMove (Some id, hto)
       | IDENT "intro"; hto = move_location -> TacIntroMove (None, hto)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 4c6afba11..1535bab9a 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -665,8 +665,6 @@ and pr_atom1 = function
   | TacIntroPattern (_::_ as p) ->
       hov 1 (str "intros" ++ spc () ++
              prlist_with_sep spc Miscprint.pr_intro_pattern p)
-  | TacIntrosUntil h ->
-      hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
   | TacIntroMove (None,MoveLast) as t -> pr_atom0 t
   | TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
   | TacIntroMove (ido,hto) ->
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index a07069bd3..d49040fc0 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 0697ae552..2937d4273 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 80711cf81..60bc784f1 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 0432b08ec..95752c99a 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 0ff4fe9b8..4bf2e5fb8 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)