From 099ed72c853e31e9ead230ded55cfb1d09528c77 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 15 May 2014 10:26:32 +0200
Subject: Polymorphic Lemmas are like Defined ones for STM

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

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index fcfd616f4..f51f5d2a0 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -48,7 +48,7 @@ let elide_part_of_script_and_now (a, _) =
 
 let make_polymorphic (a, b as x) =
   match a with
-  | VtStartProof (x, y, ids, _) -> (VtStartProof (x, y, ids, true), b)
+  | VtStartProof (x, _, ids, _) -> (VtStartProof (x, Doesn'tGuaranteeOpacity, ids, true), b)
   | _ -> x
 
 let undo_classifier = ref (fun _ -> assert false)
-- 
cgit v1.2.3