aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-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 b317cec0d..3e4f67498 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -167,7 +167,7 @@ VERNAC COMMAND EXTEND Function
(Vernacexpr.VernacFixpoint(None, List.map snd recsl))
with
| Vernacexpr.VtSideff ids, _ when hard ->
- Vernacexpr.VtStartProof ("Classic", ids), Vernacexpr.VtLater
+ Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
| x -> x ]
-> [ do_generate_principle false (List.map snd recsl) ]
END