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.

---
 stm/lemmas.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 8db8de9927..ce5ef01699 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -385,7 +385,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
 let rec_tac_initializer finite guard thms snl =
   if finite then
     match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
-    | (id,_)::l -> Proofview.V82.tactic (Tactics.mutual_cofix id l 0)
+    | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
     (* nl is dummy: it will be recomputed at Qed-time *)
-- 
cgit v1.2.3