Moving the "cofix" tactic to TACTIC EXTEND.

7 files changed, 7 insertions, 17 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 3993f1b37..33a96150c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -146,7 +146,6 @@ type 'a gen_atomic_tactic_expr =
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
-  | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
       bool * 'tacexpr option *
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 497819b32..6c3918be3 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -557,8 +557,6 @@ GEXTEND Gram
       | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl)
       | "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)
-      | "cofix"; id = ident -> TacAtom (!@loc, TacCofix (Some id))
       | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
 	  TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd))
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index fe0be9b25..05c3b3bf4 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -832,8 +832,6 @@ module Make
             hov 1 (
               primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
               ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
-          | TacCofix ido ->
-            hov 1 (primitive "cofix" ++ pr_opt pr_id ido)
           | TacMutualCofix (id,l) ->
             hov 1 (
               primitive "cofix" ++ spc () ++ pr_id id ++ spc()
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index c6f59f79e..27efc06cc 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -199,6 +199,13 @@ TACTIC EXTEND fix
 | [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ]
 END
 
+(* Cofix *)
+
+TACTIC EXTEND cofix
+  [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ]
+| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ]
+END
+
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
 open Tacexpr
@@ -217,7 +224,6 @@ let initial_atomic () =
         "compute", TacReduce(Cbv Redops.all_flags,nocl);
         "intro", TacIntroMove(None,MoveLast);
         "intros", TacIntroPattern [];
-        "cofix", TacCofix None;
       ]
   in
   let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index b4a595b05..e7545597c 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -494,7 +494,6 @@ let rec intern_atomic lf ist x =
   | 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)
-  | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f74ea4fc9..2a741ee36 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1764,15 +1764,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
-  | TacCofix idopt ->
-      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
-          (TacCofix (idopt))
-          (Proofview.V82.tactic (Tactics.cofix idopt))
-      end }
   | TacMutualCofix (id,l) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index f611f0368..faf068bfd 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -148,7 +148,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb)
   | 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
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
   | TacAssert (b,otac,na,c) ->