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/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 84ffb84206..f4b0015851 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
 let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
   let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
   if program_mode then
-    let hook _ vis gr =
+    let hook _ _ vis gr =
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
       Impargs.declare_manual_implicits false gr ~enriching:false [imps];
       let pri = intern_info pri in
-- 
cgit v1.2.3