diff options
author | Vincent Laporte <Vincent.Laporte@gmail.com> | 2017-12-12 15:32:59 +0000 |
---|---|---|
committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-08 13:33:23 +0000 |
commit | ab8e47207245277cb5b92b80a92ae78ede5bfafe (patch) | |
tree | ec968b32532e3e8d67f9b7886853a288a43aac19 /plugins/funind/g_indfun.ml4 | |
parent | 557f017f2decd056cb04a6b87719a9d82c80a425 (diff) |
[vernac] vernac_expr no longer recursive
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 1 insertions, 1 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) |