Instead of relying on a trick to make the constructor tactic parse, put

all the tactics using the constructor keyword in one entry. This has the
side-effect to also remove the other variant of constructor from the AST.

I also needed to hack around the "tauto" tactic to make it work, by
calling directly the ML tactic through a TacExtend node. This may be
generalized to get rid of the intermingled dependencies between this
tactic and the infamous Ltac quotation mechanism.

10 files changed, 31 insertions, 39 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 32001e629..67331727a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -390,10 +390,6 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacSplit (ev,l) ->
       <:expr< Tacexpr.TacSplit
         ($mlexpr_of_bool ev$, $mlexpr_of_list mlexpr_of_binding_kind l$)>>
-  | Tacexpr.TacConstructor (ev,n,l) ->
-      let n = mlexpr_of_or_var mlexpr_of_int n in
-      <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $mlexpr_of_binding_kind l$>>
-
   (* Conversion *)
   | Tacexpr.TacReduce (r,cl) ->
       let l = mlexpr_of_clause cl in
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 3b5868e9e..88e5c3696 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -149,7 +149,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
 
   (* Trmuctors *)
   | TacSplit of evars_flag * 'trm bindings list
-  | TacConstructor of evars_flag * int or_var * 'trm bindings
 
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c32ade38c..b9eaf53ee 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -645,10 +645,6 @@ GEXTEND Gram
       | "exists"; bll = opt_bindings -> TacSplit (false,bll)
       | IDENT "eexists"; bll = opt_bindings ->
 	  TacSplit (true,bll)
-      | IDENT "constructor"; n = nat_or_var; l = with_bindings ->
-	  TacConstructor (false,n,l)
-      | IDENT "econstructor"; n = nat_or_var; l = with_bindings ->
-	  TacConstructor (true,n,l)
       (* Equivalence relations *)
       | IDENT "symmetry"; "in"; cl = in_clause -> TacSymmetry cl
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 24f374b17..cdcff9bb2 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -778,10 +778,6 @@ and pr_atom1 = function
 
   (* Constructors *)
   | TacSplit (ev,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l)
-  | TacConstructor (ev,n,l) ->
-      hov 1 (str (with_evars ev "constructor") ++
-             pr_or_var pr_intarg n ++ pr_bindings l)
-
   (* Conversion *)
   | TacReduce (r,h) ->
       hov 1 (pr_red_expr r ++
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 731c6df06..196507274 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -106,10 +106,30 @@ END
 
 TACTIC EXTEND constructor
   [ "constructor" ] -> [ Tactics.any_constructor false None ]
+| [ "constructor" int_or_var(i) ] -> [
+    let i = Tacinterp.interp_int_or_var ist i in
+    Tactics.constructor_tac false None i NoBindings
+  ]
+| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
+    let { Evd.sigma = sigma; it = bl } = bl in
+    let i = Tacinterp.interp_int_or_var ist i in
+    let tac c = Tactics.constructor_tac false None i c in
+    Tacticals.New.tclWITHHOLES false tac sigma bl
+  ]
 END
 
 TACTIC EXTEND econstructor
   [ "econstructor" ] -> [ Tactics.any_constructor true None ]
+| [ "econstructor" int_or_var(i) ] -> [
+    let i = Tacinterp.interp_int_or_var ist i in
+    Tactics.constructor_tac true None i NoBindings
+  ]
+| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
+    let { Evd.sigma = sigma; it = bl } = bl in
+    let i = Tacinterp.interp_int_or_var ist i in
+    let tac c = Tactics.constructor_tac true None i c in
+    Tacticals.New.tclWITHHOLES true tac sigma bl
+  ]
 END
 
 (** Specialize *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 197caf3bd..6c9e20289 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -523,7 +523,6 @@ let rec intern_atomic lf ist x =
 
   (* Constructors *)
   | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll)
-  | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a393ea4f6..2bb8ab840 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1760,15 +1760,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
         Tacticals.New.tclWITHHOLES ev (Tactics.split_with_bindings ev) sigma bll
       end
-  | TacConstructor (ev,n,bl) ->
-      Proofview.Goal.raw_enter begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = Proofview.Goal.sigma gl in
-        let sigma, bl = interp_bindings ist env sigma bl in
-        Tacticals.New.tclWITHHOLES ev
-          (Tactics.constructor_tac ev None (interp_int_or_var ist n)) sigma bl
-      end
-
   (* Conversion *)
   | TacReduce (r,cl) ->
       Proofview.V82.tactic begin fun gl -> 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d0894d76f..d8ff931d3 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -181,7 +181,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 
   (* Constructors *)
   | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll)
-  | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index bdacf85a8..4f0bc5848 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -153,6 +153,11 @@ let flatten_contravariant_conj flags ist =
 
 (** Dealing with disjunction *)
 
+let constructor i =
+  let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
+  let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
+  Tacexpr.TacAtom (Loc.ghost, Tacexpr.TacExtend (Loc.ghost, name, [i]))
+
 let is_disj flags ist =
   let t = assoc_var "X1" ist in
   if (not flags.binary_mode_bugged_detection || bugged_is_binary t) &&
@@ -176,12 +181,11 @@ let flatten_contravariant_disj flags ist =
       let hyp = valueIn (Value.of_constr hyp) in
       iter_tac (List.map_i (fun i arg ->
 	let typ = valueIn (Value.of_constr (mkArrow arg c)) in
-	let i = Tacexpr.TacGeneric (in_gen (rawwit wit_int) i) in
+	let ci = constructor i in
 	<:tactic<
           let typ := $typ in
           let hyp := $hyp in
-	  let i := $i in
-	  assert typ by (intro; apply hyp; constructor i; assumption)
+	  assert typ by (intro; apply hyp; $ci; assumption)
 	>>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
   | _ ->
       <:tactic<fail>>
@@ -199,9 +203,10 @@ let not_dep_intros ist =
 let axioms flags ist =
   let t_is_unit_or_eq = tacticIn (is_unit_or_eq flags)
   and t_is_empty = tacticIn is_empty in
+  let c1 = constructor 1 in
     <:tactic<
     match reverse goal with
-      | |- ?X1 => $t_is_unit_or_eq; constructor 1
+      | |- ?X1 => $t_is_unit_or_eq; $c1
       | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
       | _:?X1 |- ?X1 => assumption
     end >>
@@ -214,6 +219,7 @@ let simplif flags ist =
   and t_flatten_contravariant_disj = tacticIn (flatten_contravariant_disj flags)
   and t_is_disj = tacticIn (is_disj flags)
   and t_not_dep_intros = tacticIn not_dep_intros in
+  let c1 = constructor 1 in
   <:tactic<
     $t_not_dep_intros;
     repeat
@@ -231,7 +237,7 @@ let simplif flags ist =
           $t_is_unit_or_eq; cut X2;
 	    [ intro; clear id
 	    | (* id : forall (_: ?X1), ?X2 |- ?X2 *)
-	      cut X1; [exact id| constructor 1; fail]
+	      cut X1; [exact id| $c1; fail]
 	    ]
         | id: forall (_ : ?X1), ?X2|- _ =>
           $t_flatten_contravariant_conj
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index fbad368c2..5095329cd 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -90,13 +90,3 @@ Declare ML Module "g_class".
 Declare ML Module "g_eqdecide".
 Declare ML Module "g_rewrite".
 Declare ML Module "tauto".
-
-(** Small hack to overcome the fact that the (e)constructor tactics need to have
-    a proper parsing rule, because the variants with arguments conflicts
-    with it. *)
-Module CoreTactics.
-Declare ML Module "coretactics".
-End CoreTactics.
-
-Tactic Notation "constructor" := CoreTactics.constructor.
-Tactic Notation "econstructor" := CoreTactics.econstructor.