Moving argument-free tactics out of the AST into a dedicated

"coretactics.ml4" file.

6 files changed, 21 insertions, 8 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
new file mode 100644
index 0000000000..0170b68014
--- /dev/null
+++ b/tactics/coretactics.ml4
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+DECLARE PLUGIN "coretactics"
+
+TACTIC EXTEND reflexivity
+  [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
+END
+
+TACTIC EXTEND assumption
+  [ "assumption" ] -> [ Tactics.assumption ]
+END
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index bc94c722f5..ff2e1ff6aa 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,4 +1,5 @@
 Extraargs
+Coretactics
 Extratactics
 Eauto
 Class_tactics
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 9259048260..2a6589d21f 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -77,7 +77,6 @@ let initial_atomic =
         "compute", TacReduce(Cbv Redops.all_flags,nocl);
         "intro", TacIntroMove(None,MoveLast);
         "intros", TacIntroPattern [];
-        "assumption", TacAssumption;
         "cofix", TacCofix None;
         "trivial", TacTrivial (Off,[],None);
         "auto", TacAuto(Off,None,[],None);
@@ -89,7 +88,6 @@ let initial_atomic =
         "esplit", TacSplit(true,false,[NoBindings]);
         "constructor", TacAnyConstructor (false,None);
         "econstructor", TacAnyConstructor (true,None);
-        "reflexivity", TacReflexivity;
         "symmetry", TacSymmetry nocl
       ]
   in
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index fa76b2a94b..ea3e346853 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -455,7 +455,6 @@ let rec intern_atomic lf ist x =
   | TacIntroMove (ido,hto) ->
       TacIntroMove (Option.map (intern_ident lf ist) ido,
                     intern_move_location ist hto)
-  | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (intern_constr ist c)
   | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
   | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
@@ -559,7 +558,6 @@ let rec intern_atomic lf ist x =
 	clause_app (intern_hyp_location ist) cl)
 
   (* Equivalence relations *)
-  | TacReflexivity -> TacReflexivity
   | TacSymmetry idopt ->
       TacSymmetry (clause_app (intern_hyp_location ist) idopt)
   | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 69505172cb..d72a37d33e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1447,7 +1447,6 @@ and interp_atomic ist tac =
         let mloc = interp_move_location ist env hto in
         Tactics.intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
       end
-  | TacAssumption -> Tactics.assumption
   | TacExact c ->
       Proofview.V82.tactic begin fun gl -> 
         let (sigma,c_interp) = pf_interp_casted_constr ist gl c in
@@ -1793,7 +1792,6 @@ and interp_atomic ist tac =
       end
 
   (* Equivalence relations *)
-  | TacReflexivity -> Tactics.intros_reflexivity
   | TacSymmetry c ->
       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 47fa4f9424..31a1b57bc0 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -134,7 +134,6 @@ 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
-  | TacAssumption as x -> x
   | TacExact c -> TacExact (subst_glob_constr subst c)
   | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c)
   | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c)
@@ -201,7 +200,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
         subst_glob_constr subst c, cl)
 
   (* Equivalence relations *)
-  | TacReflexivity | TacSymmetry _ as x -> x
+  | TacSymmetry _ as x -> x
   | TacTransitivity c -> TacTransitivity (Option.map (subst_glob_constr subst) c)
 
   (* Equality and inversion *)