From 12f4c8ed277fa8368cab2e99f173339a64bcef3d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 18:34:21 +0200
Subject: Put the "fix" 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 4e2dfafb52..98b77ab357 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -231,8 +231,8 @@ 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) ]
+  [ "fix" natural(n) ] -> [ Tactics.fix None n ]
+| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ]
 END
 
 (* Cofix *)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index d650cb5c6f..5e0153fcee 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1714,7 +1714,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_fix (interp_ident ist env sigma id) n l_interp 0) in
+        let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
-- 
cgit v1.2.3