From a084c94b7402bce8b5b55843b4dee4e65f842bbf Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 4 Dec 2013 17:13:52 +0100
Subject: Fix g_derive.ml4.

My bad, I forgot to fix the classification before comitting.---
 plugins/Derive/g_derive.ml4 | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4
index 354643c092..9137c3d282 100644
--- a/plugins/Derive/g_derive.ml4
+++ b/plugins/Derive/g_derive.ml4
@@ -8,9 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
-(* arnaud: on a sans doute besoin des noms dans la liste. *)
-(* arnaud: est-ce que VtNow signifie bien qu'on ne peut pas skipper la preuve? *)
-let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtNow)
+let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),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