From 9cb970f99c0bd5f033742154c11c8313800de960 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 31 Oct 2018 16:45:43 +0100
Subject: [program] extend obligation to give back a mapping from obligations
 to terms

This is necessary for programs like Equations that call add_definition
and want to later update in their hook some separate datastructures
which refer to the obligations that are defined by Program. We give back
a map from obligation name to a constr defined in the program's universe
state which the hook returns as well. (Obligation names also correspond
to undefined evars in the original terms through
Obligations.eterm_obligations).

Using this, I can avoid ucontext_of_aucontext in Equations, allowing PR
 #8601 to go through.
---
 vernac/comDefinition.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comDefinition.ml')

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
-- 
cgit v1.2.3