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/comProgramFixpoint.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index fe8ef1f0e0..3d3d825bd0 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -193,7 +193,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       let name = add_suffix recname "_func" in
       (* XXX: Mutating the evar_map in the hook! *)
       (* XXX: Likely the sigma is out of date when the hook is called .... *)
-      let hook sigma _ l gr =
+      let hook sigma _ _ l gr =
         let sigma, h_body = Evarutil.new_global sigma gr in
         let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
@@ -212,7 +212,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       hook, name, typ
     else
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook sigma _ l gr =
+      let hook sigma _ _ l gr =
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
-- 
cgit v1.2.3