Removing the "constructor" tactic from the AST.

5 files changed, 10 insertions, 6 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index d49040fc02..731c6df067 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 1ab0efae78..62b9904d7b 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 62f7d4d653..197caf3bd0 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 c346a7cd35..a393ea4f6d 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 4bf2e5fb83..d0894d76f9 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 *)