diff options
| author | Pierre-Marie Pédrot | 2015-02-15 18:17:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-15 18:17:04 +0100 |
| commit | d7691de7184b4cdcfd48fd762011569cde5523c5 (patch) | |
| tree | 9c9e14226b070fc2a5cf4c216c4f8c634de20855 /plugins/funind/invfun.ml | |
| parent | eed12bddc3e6f6f9192c909a8b8f82859080f3a1 (diff) | |
| parent | aed3c876d422f4dcc0296fd4949148c697f37b1d (diff) | |
Merge branch 'v8.5'
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 |