diff options
| author | Pierre-Marie Pédrot | 2018-11-06 18:40:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-06 18:40:20 +0100 |
| commit | 92d1a0c14ef326929b6870541073bcae4d2c895d (patch) | |
| tree | 4e4e722b7d8881ad29d790a4a0dfd24a7e8a4226 /vernac/comDefinition.ml | |
| parent | f6033667bd9b8069308d4bcba420c4ce0771e44f (diff) | |
| parent | 05336f66483eec4c34f19df937d28b8bdae8749a (diff) | |
Merge PR #8889: Program hook gives back an obligation substitiution
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index cc03473bc6..472411ac3a 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -109,7 +109,7 @@ let do_definition ~program_mode ident k univdecl 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 = Obligations.mk_univ_hook (fun _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in + let hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in ignore(Obligations.add_definition ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in |