aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-05-15 10:50:05 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-05-15 10:52:53 +0200
commit49542cf365715e27811cc15d99565046d8754c20 (patch)
tree6fbbaea0000eef2163d387467bbd771d3f67ea92 /plugins
parent099ed72c853e31e9ead230ded55cfb1d09528c77 (diff)
poly: remove unused attribute to STM nodes and vernac classificaiton
Diffstat (limited to 'plugins')
-rw-r--r--plugins/Derive/g_derive.ml42
-rw-r--r--plugins/funind/g_indfun.ml42
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4
index c7db26fb8..9137c3d28 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,[], false),VtLater)
+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) ] ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 21d0b9f3d..d77385321 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -165,7 +165,7 @@ VERNAC COMMAND EXTEND Function
(Vernacexpr.VernacFixpoint(None, List.map snd recsl))
with
| Vernacexpr.VtSideff ids, _ when hard ->
- Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids, false), VtLater)
+ Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
| x -> x ]
-> [ do_generate_principle false (List.map snd recsl) ]
END