diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2013-11-27 14:11:03 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2013-12-04 14:14:32 +0100 |
| commit | 358a68a90416facf4f149c98332e8118971d4793 (patch) | |
| tree | 80f3dbc522c94f113e101fd32fb801028b8d93e5 /plugins/funind/invfun.ml | |
| parent | db65876404c7c3a1343623cc9b4d6c2a7164dd95 (diff) | |
The commands that initiate proofs are now in charge of what happens when proofs end.
The proof ending commands like Qed and Defined had all the control on what happened to the proof when they are closed. In constrast, proof starting commands were dumb: start a proof, give it a name, that's it.
In such a situation if we want to come up with new reasons to open proofs, we would need new proof-closing commands.
In this commit we decide at proof-starting time how to dispatch the various Qed/Defined, etc… By registering a function in the interactive proof environment. This way, proofs are always closed the same but we can invent new ways to start them.
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 0d32bf2bc..7c8f5714e 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1008,7 +1008,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = -let do_save () = Lemmas.save_named false +let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None)) (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness |