diff options
| author | Matthieu Sozeau | 2014-05-06 10:13:10 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 10:13:10 +0200 |
| commit | 0857007106234d46e1b30170f36635ad631653c6 (patch) | |
| tree | 0cad3a121b5e94e4d3f7c9d0dc7e2874b05b2b16 /toplevel | |
| parent | 8fba83723e142696c480843a318a3959ed9ed87c (diff) | |
Cleanup before merge with the trunk
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/g_obligations.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 index 2354aa3325..061f7ba5d8 100644 --- a/toplevel/g_obligations.ml4 +++ b/toplevel/g_obligations.ml4 @@ -54,7 +54,7 @@ GEXTEND Gram open Obligations -let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater) +let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[],false), VtLater) VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl | [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> |