aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2017-12-12 15:32:59 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-01-08 13:33:23 +0000
commitab8e47207245277cb5b92b80a92ae78ede5bfafe (patch)
treeec968b32532e3e8d67f9b7886853a288a43aac19 /plugins
parent557f017f2decd056cb04a6b87719a9d82c80a425 (diff)
[vernac] vernac_expr no longer recursive
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/ssr/ssrvernac.ml44
3 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 2fd6f53c4..4b828a702 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function
| _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
- (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+ (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
with
| Vernacexpr.VtSideff ids, _ when hard ->
Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index b4e17c5d1..0b929b8ca 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1509,7 +1509,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
msg
in
@@ -1524,7 +1524,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 4f530a0ae..c0479dd24 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -551,9 +551,9 @@ GEXTEND Gram
| IDENT "Canonical"; qid = Constr.global;
d = G_vernac.def_body ->
let s = coerce_reference_to_id qid in
- Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition
+ Vernacexpr.VernacDefinition
((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
- ((Loc.tag s),None),(d )))
+ ((Loc.tag s),None), d)
]];
END