10 files changed, 20 insertions, 18 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 1614301ec..32001e629 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -390,8 +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.TacAnyConstructor (ev,t) ->
-      <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>>
   | 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$>>
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7f7ecdcf7..3b5868e9e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -149,8 +149,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
 
   (* Trmuctors *)
   | TacSplit of evars_flag * 'trm bindings list
-  | TacAnyConstructor of evars_flag *
-      ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option
   | TacConstructor of evars_flag * int or_var * 'trm bindings
 
   (* Conversion *)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 29cb45ad1..c32ade38c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -649,9 +649,6 @@ GEXTEND Gram
 	  TacConstructor (false,n,l)
       | IDENT "econstructor"; n = nat_or_var; l = with_bindings ->
 	  TacConstructor (true,n,l)
-      | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor (false,t)
-      | IDENT "econstructor"; t = OPT tactic -> TacAnyConstructor (true,t)
-
       (* Equivalence relations *)
       | IDENT "symmetry"; "in"; cl = in_clause -> TacSymmetry cl
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 1535bab9a..24f374b17 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -646,8 +646,6 @@ let pr_cofix_tac (id,c) =
 let rec pr_atom0 = function
   | TacIntroPattern [] -> str "intros"
   | TacIntroMove (None,MoveLast) -> str "intro"
-  | TacAnyConstructor (false,None) -> str "constructor"
-  | TacAnyConstructor (true,None) -> str "econstructor"
   | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial")
   | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto")
   | TacClear (true,[]) -> str "clear"
@@ -780,9 +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)
-  | TacAnyConstructor (ev,Some t) ->
-      hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t)
-  | TacAnyConstructor (ev,None) as t -> pr_atom0 t
   | TacConstructor (ev,n,l) ->
       hov 1 (str (with_evars ev "constructor") ++
              pr_or_var pr_intarg n ++ pr_bindings l)
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index d49040fc0..731c6df06 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -102,6 +102,16 @@ TACTIC EXTEND eright_with
   ]
 END
 
+(** Constructor *)
+
+TACTIC EXTEND constructor
+  [ "constructor" ] -> [ Tactics.any_constructor false None ]
+END
+
+TACTIC EXTEND econstructor
+  [ "econstructor" ] -> [ Tactics.any_constructor true None ]
+END
+
 (** Specialize *)
 
 TACTIC EXTEND specialize
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 1ab0efae7..62b9904d7 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -94,8 +94,6 @@ let initial_atomic =
         "cofix", TacCofix None;
         "trivial", TacTrivial (Off,[],None);
         "auto", TacAuto(Off,None,[],None);
-        "constructor", TacAnyConstructor (false,None);
-        "econstructor", TacAnyConstructor (true,None);
       ]
   in
   let fold accu (s, t) = Id.Map.add (Id.of_string s) t accu in
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 62f7d4d65..197caf3bd 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)
-  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_pure_tactic ist) t)
   | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl)
 
   (* Conversion *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c346a7cd3..a393ea4f6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1760,8 +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
-  | TacAnyConstructor (ev,t) ->
-      Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
   | TacConstructor (ev,n,bl) ->
       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 4bf2e5fb8..d0894d76f 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)
-  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
   | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
 
   (* Conversion *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 5095329cd..fbad368c2 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -90,3 +90,13 @@ 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.