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

"coretactics.ml4" file.

11 files changed, 22 insertions, 19 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 9a0a22b9f1..abc0d31a93 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -308,8 +308,6 @@ let rec mlexpr_of_atomic_tactic = function
       let idopt = mlexpr_of_ident_option idopt in
       let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in
       <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >>
-  | Tacexpr.TacAssumption ->
-      <:expr< Tacexpr.TacAssumption >>
   | Tacexpr.TacExact c ->
       <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
   | Tacexpr.TacExactNoCheck c ->
@@ -420,7 +418,6 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacChange $g p$ $mlexpr_of_constr c$ $l$ >>
 
   (* Equivalence relations *)
-  | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>
   | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
   | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 16b1dc5eb1..532786fd37 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -105,7 +105,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacIntroPattern of intro_pattern_expr located list
   | TacIntrosUntil of quantified_hypothesis
   | TacIntroMove of Id.t option * 'nam move_location
-  | TacAssumption
   | TacExact of 'trm
   | TacExactNoCheck of 'trm
   | TacVmCastNoCheck of 'trm
@@ -163,7 +162,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacChange of 'pat option * 'trm * 'nam clause_expr
 
   (* Equivalence relations *)
-  | TacReflexivity
   | TacSymmetry of 'nam clause_expr
   | TacTransitivity of 'trm option
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 65e046fb86..d1620ca8a7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -532,7 +532,6 @@ GEXTEND Gram
       | IDENT "intro"; id = ident -> TacIntroMove (Some id, MoveLast)
       | IDENT "intro" -> TacIntroMove (None, MoveLast)
 
-      | IDENT "assumption" -> TacAssumption
       | IDENT "exact"; c = constr -> TacExact c
       | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
       | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
@@ -658,7 +657,6 @@ GEXTEND Gram
       | IDENT "econstructor"; t = OPT tactic -> TacAnyConstructor (true,t)
 
       (* Equivalence relations *)
-      | IDENT "reflexivity" -> TacReflexivity
       | IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl
       | IDENT "transitivity"; c = constr -> TacTransitivity (Some c)
       | IDENT "etransitivity" -> TacTransitivity None
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index ffb0d7a369..c7644f8c60 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -623,12 +623,10 @@ let pr_cofix_tac (id,c) =
 let rec pr_atom0 = function
   | TacIntroPattern [] -> str "intros"
   | TacIntroMove (None,MoveLast) -> str "intro"
-  | TacAssumption -> str "assumption"
   | 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")
-  | TacReflexivity -> str "reflexivity"
   | TacClear (true,[]) -> str "clear"
   | t -> str "(" ++ pr_atom1 t ++ str ")"
 
@@ -651,7 +649,6 @@ and pr_atom1 = function
   | TacIntroMove (ido,hto) ->
       hov 1 (str"intro" ++ pr_opt pr_id ido ++
              Miscprint.pr_move_location pr_ident hto)
-  | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
   | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
@@ -799,7 +796,6 @@ and pr_atom1 = function
       pr_constr c ++ pr_clauses (Some true) pr_ident h)
 
   (* Equivalence relations *)
-  | TacReflexivity as x -> pr_atom0 x
   | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr_ident cls
   | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c
   | TacTransitivity None -> str "etransitivity"
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 *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 7cf478e183..5095329cd2 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -83,6 +83,7 @@ Open Scope type_scope.
 
 (** ML Tactic Notations *)
 
+Declare ML Module "coretactics".
 Declare ML Module "extratactics".
 Declare ML Module "eauto".
 Declare ML Module "g_class".