Moving the "fix" tactic to TACTIC EXTEND.

7 files changed, 7 insertions, 15 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 502f2db4c1..3993f1b371 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -145,7 +145,6 @@ type 'a gen_atomic_tactic_expr =
       ('nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
-  | TacFix of Id.t option * int
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 77b7b05a39..497819b327 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -555,8 +555,6 @@ GEXTEND Gram
           TacAtom (!@loc, TacElim (true,cl,el))
       | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl)
       | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl)
-      | "fix"; n = natural -> TacAtom (!@loc, TacFix (None,n))
-      | "fix"; id = ident; n = natural -> TacAtom (!@loc, TacFix (Some id,n))
       | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
 	  TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd))
       | "cofix" -> TacAtom (!@loc, TacCofix None)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 12667d0f24..fe0be9b255 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -828,7 +828,6 @@ module Make
               ++ pr_opt pr_eliminator cbo)
           | TacCase (ev,cb) ->
             hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
-          | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
           | TacMutualFix (id,n,l) ->
             hov 1 (
               primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 63fb67e146..c6f59f79e3 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -192,6 +192,13 @@ TACTIC EXTEND admit
  [ "admit" ] -> [ Proofview.give_up ]
 END
 
+(* Fix *)
+
+TACTIC EXTEND fix
+  [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ]
+| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ]
+END
+
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
 open Tacexpr
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index cbb9db65c1..b4a595b051 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -491,7 +491,6 @@ let rec intern_atomic lf ist x =
       TacElim (ev,intern_constr_with_bindings_arg ist cb,
                Option.map (intern_constr_with_bindings ist) cbo)
   | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings_arg ist cb)
-  | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
       TacMutualFix (intern_ident lf ist id, n, List.map f l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d5a1215b87..f74ea4fc9b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1749,15 +1749,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         Tacticals.New.tclWITHHOLES ev named_tac sigma
       end }
-  | TacFix (idopt,n) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let idopt = Option.map (interp_ident ist env sigma) idopt in
-        name_atomic ~env
-          (TacFix(idopt,n))
-          (Proofview.V82.tactic (Tactics.fix idopt n))
-      end }
   | TacMutualFix (id,n,l) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 4a5fa9828e..f611f03684 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -146,7 +146,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       TacElim (ev,subst_glob_with_bindings_arg subst cb,
                Option.map (subst_glob_with_bindings subst) cbo)
   | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb)
-  | TacFix (idopt,n) as x -> x
   | TacMutualFix (id,n,l) ->
       TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
   | TacCofix idopt as x -> x