Browse files

Fix g_derive.ml4.

My bad, I forgot to fix the classification before comitting.
  • Loading branch information...
1 parent 1fb883a commit a084c94b7402bce8b5b55843b4dee4e65f842bbf @aspiwack aspiwack committed Dec 4, 2013
Showing with 1 addition and 3 deletions.
  1. +1 −3 plugins/Derive/g_derive.ml4
View
4 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) ] ->

0 comments on commit a084c94

Please sign in to comment.