diff options
| author | Emilio Jesus Gallego Arias | 2019-06-17 04:34:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-26 01:15:49 +0200 |
| commit | 81494db46137b2934167ae12d0b86e27e28023e9 (patch) | |
| tree | ad2a7b85cde2409debfd5f0650c3b70c467c7a7a /vernac/comProgramFixpoint.ml | |
| parent | 2433d810b9850d25819f97643664a851d29d2e0f (diff) | |
[declare] Fine tuning of Hook type.
We turn the hook parameter into a record, making more explicit the
capture of data in hooks as they only take one parameter now
This is a fine-tuning but provides some small advantages, and allows
us to tweak the hook type with less breakage.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index d804957917..3947bb1b14 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -204,8 +204,8 @@ let build_wellfounded (recname,pl,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 sigma, h_body = Evarutil.new_global sigma gr in + let hook sigma { DeclareDef.Hook.S.dref; _ } = + let sigma, h_body = Evarutil.new_global sigma dref 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 let ty = EConstr.Unsafe.to_constr ty in @@ -222,9 +222,9 @@ let build_wellfounded (recname,pl,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 { DeclareDef.Hook.S.dref; _ } = if Impargs.is_implicit_args () || not (List.is_empty impls) then - Impargs.declare_manual_implicits false gr impls + Impargs.declare_manual_implicits false dref impls in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) |