diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-30 19:32:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-30 19:35:49 +0100 |
| commit | 35afb42a6bb30634d2eb77a32002ed473633b5f4 (patch) | |
| tree | 464483d6ef42aa817793297c5ac146d4b68307d8 /toplevel | |
| parent | bf1eef119ef8f0e6a2ae4b66165d6e22c1ce9236 (diff) | |
| parent | b49c80406f518d273056b2143f55e23deeea2813 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 3 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 14 |
2 files changed, 10 insertions, 7 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 73fd3d1a4..3d338ee0a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -154,6 +154,7 @@ let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook let declare_definition ident (local, p, k) ce pl imps hook = + let fix_exn = Future.fix_exn_of ce.const_entry_body in let () = !declare_definition_hook ce in let r = match local with | Discharge when Lib.sections_are_opened () -> @@ -170,7 +171,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = gr | Discharge | Local | Global -> declare_global_definition ident ce local k pl imps in - Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r + Lemmas.call_hook fix_exn hook local r let _ = Obligations.declare_definition_ref := (fun i k c imps hook -> declare_definition i k c [] imps hook) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 0e2de74aa..de03e8356 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -508,16 +508,17 @@ let declare_definition prg = let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in + let fix_exn = Stm.get_fix_exn () in let ce = - definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) + definition_entry ~fix_exn + ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) + ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in progmap_remove prg; !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits - (Lemmas.mk_hook (fun l r -> - Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r)) - + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r)) + open Pp let rec lam_index n t acc = @@ -620,8 +621,9 @@ let declare_obligation prg obl body ty uctx = if get_shrink_obligations () && not poly then shrink_body body else [], body, [||] in + let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let ce = - { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants); + { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = if List.is_empty ctx then ty else None; const_entry_polymorphic = poly; |