diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-02 10:52:31 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-08 11:17:05 +0200 |
| commit | 289b2b9a1c3d3ebc3c1975663d16c04e88b6329b (patch) | |
| tree | b8484b831d9fe3d027c186ebe86acbc82426fea3 /plugins/funind/indfun_common.mli | |
| parent | e1ba72037191b1d4be9de8a0a8fc1faa24eeb12c (diff) | |
Enforce a correct exception handling in declaration_hooks
This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 6e8b79a6b..3fafeadc1 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val const_of_id: Id.t -> constant val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr -val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> +val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> unit Tacexpr.declaration_hook Ephemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and |