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.ml | |
| 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.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 70a892a3b..8c8d7a667 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -352,7 +352,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition) - bl None body (Some ret_type) (fun _ _ -> ()) + bl None body (Some ret_type) (Future.mk_hook (fun _ _ -> ())) | _ -> Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl |