From 755dd6ce7140e849fcd44c1c4ce2e265776b2c6a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Nov 2014 21:54:15 +0100
Subject: Writing the raw introduction tactic in the new monad.

---
 plugins/micromega/coq_micromega.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a6d2cf75c4..db22727fc4 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1403,7 +1403,7 @@ let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic =
      ]
      (Tacmach.pf_concl gl)) gl);
   Tactics.generalize env ;
-  Tacticals.tclTHENSEQ (List.map Tactics.introduction ids) ; 
+  Tacticals.tclTHENSEQ (List.map (fun id -> Proofview.V82.of_tactic (Tactics.introduction id)) ids) ; 
  ] 
 
 
-- 
cgit v1.2.3