diff options
| author | Matthieu Sozeau | 2018-10-31 16:45:43 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-11-06 12:09:26 +0100 |
| commit | 9cb970f99c0bd5f033742154c11c8313800de960 (patch) | |
| tree | 63efcec372dbfd0401f72cd8d5120a5760fe5e33 /vernac/comProgramFixpoint.ml | |
| parent | 1aa71f100ddd5e3651a7d6e4adf0ebba5ae5fdee (diff) | |
[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.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |