diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c7b0a0b08..b9d7e0d909 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1022,7 +1022,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = -let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None)) +let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))) (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness |