From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 28 Oct 2013 14:08:46 +0100
Subject: Initial work on reintroducing old-style polymorphism for
 compatibility (the stdlib does not compile entirely).

---
 plugins/Derive/g_derive.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/Derive')

diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4
index 9137c3d282..c7db26fb87 100644
--- a/plugins/Derive/g_derive.ml4
+++ b/plugins/Derive/g_derive.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
-let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
+let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[], false),VtLater)
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command
 | [ "Derive" ident(f) "From" constr(init) "Upto" constr(r) "As" ident(lemma) ] ->
-- 
cgit v1.2.3