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/indfun_common.mli | |
| 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/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 722f857b3..cea5ffe25 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,12 +46,6 @@ val const_of_id: Id.t -> constant val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr -(* [save_named] is a copy of [Command.save_named] but uses - [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast] -*) - -val new_save_named : bool -> unit - val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> unit Tacexpr.declaration_hook Ephemeron.key -> unit |