diff options
| author | Arnaud Spiwack | 2013-11-27 14:11:03 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-04 14:14:32 +0100 |
| commit | 358a68a90416facf4f149c98332e8118971d4793 (patch) | |
| tree | 80f3dbc522c94f113e101fd32fb801028b8d93e5 /plugins/funind/functional_principles_proofs.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/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 52ba41869a..f4e8589031 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = lemma_type (fun _ _ -> ()); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_named false + Lemmas.save_proof (Vernacexpr.Proved(false,None)) |