diff options
| author | Matthieu Sozeau | 2015-11-19 17:49:32 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-19 17:52:34 +0100 |
| commit | cfc0fc0075784e75783c9b4482fd3f4b858a44bf (patch) | |
| tree | c21ad8c78fc2613d51e50128525f09ed377ac6d8 /toplevel/command.ml | |
| parent | 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c (diff) | |
Allow program hooks to see the refined universe_context at the end of a
definition, if they manipulate structures depending on the initial state
of the context.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 3d338ee0a3..0b709a3fc4 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -192,6 +192,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = Obligations.eterm_obligations env ident evd 0 c typ in let ctx = Evd.evar_universe_context evd in + let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in @@ -1010,7 +1011,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in - let hook l gr = + let hook l gr _ = let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let pl, univs = Evd.universe_context !evdref in @@ -1026,7 +1027,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook l gr = + let hook l gr _ = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in hook, recname, typ |