Moving the "cofix" tactic to TACTIC EXTEND.

4 files changed, 7 insertions, 12 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index c6f59f79e3..27efc06cca 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 b4a595b051..e7545597cc 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 f74ea4fc9b..2a741ee367 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 f611f03684..faf068bfd5 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) ->