From 81494db46137b2934167ae12d0b86e27e28023e9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 17 Jun 2019 04:34:06 +0200
Subject: [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.
---
 vernac/comProgramFixpoint.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

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