From a4bd166bd2119a5290276f0ded44f8186ba1ecee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 21:21:42 +0200
Subject: Put the "cofix" tactic in the monad.

---
 ltac/coretactics.ml4 | 4 ++--
 ltac/tacinterp.ml    | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'ltac')

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 4893e40973..766f0714d2 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -238,8 +238,8 @@ END
 (* Cofix *)
 
 TACTIC EXTEND cofix
-  [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ]
-| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ]
+  [ "cofix" ] -> [ Tactics.cofix None ]
+| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ]
 END
 
 (* Clear *)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 7acdff9acf..5aff262aa5 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1729,7 +1729,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
-        let tac = Proofview.V82.tactic (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0) in
+        let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
-- 
cgit v1.2.3