aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/g_indfun.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
-rw-r--r--plugins/funind/g_indfun.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 829556a71..87609296b 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.VernacFixpoint(None, List.map snd recsl))
+ (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))
with
| Vernacexpr.VtSideff ids, _ when hard ->
Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)