From 5f937b2f8532b2ccf36c62557934cc2c9150005b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 06:32:00 -0400
Subject: [proof] Miscellaneous cleanup on proof info handling

After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
---
 vernac/declareDef.ml | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index fc53abdcea..b0c8fe90c4 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -34,17 +34,12 @@ module Hook = struct
 
   let make hook = CEphemeron.create hook
 
-  let call ?hook ?fix_exn x =
-    try Option.iter (fun hook -> CEphemeron.get hook x) hook
-    with e when CErrors.noncritical e ->
-      let e = Exninfo.capture e in
-      let e = Option.cata (fun fix -> fix e) e fix_exn in
-      Exninfo.iraise e
+  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
+
 end
 
 (* Locality stuff *)
 let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
-  let fix_exn = Declare.Internal.get_fix_exn ce in
   let should_suggest = ce.Declare.proof_entry_opaque &&
                        Option.is_empty ce.Declare.proof_entry_secctx in
   let dref = match scope with
@@ -65,10 +60,17 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
     match hook_data with
     | None -> ()
     | Some (hook, uctx, obls) ->
-      Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref }
+      Hook.call ~hook { Hook.S.uctx; obls; scope; dref }
   end;
   dref
 
+let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
+  let fix_exn = Declare.Internal.get_fix_exn ce in
+  try declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce
+  with exn ->
+    let exn = Exninfo.capture exn in
+    Exninfo.iraise (fix_exn exn)
+
 let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
   match possible_indexes with
   | Some possible_indexes ->
@@ -127,7 +129,7 @@ let warn_let_as_axiom =
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
                   spc () ++ strbrk "declared as an axiom.")
 
-let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
+let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
   let local = match scope with
     | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified
     | Global local -> local
@@ -139,9 +141,16 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
   let () = Impargs.maybe_declare_manual_implicits false dref impargs in
   let () = Declare.assumption_message name in
   let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in
-  let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in
+  let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in
   dref
 
+let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
+  try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
+  with exn ->
+    let exn = Exninfo.capture exn in
+    let exn = Option.cata (fun fix -> fix exn) exn fix_exn in
+    Exninfo.iraise exn
+
 (* Preparing proof entries *)
 
 let check_definition_evars ~allow_evars sigma =
-- 
cgit v1.2.3


From 56ffe818ab7706a82d79b538fdf3af8b23d95f40 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 03:07:42 -0400
Subject: [declare] [obligations] Refactor preparation of obligation entry

Preparation of obligation/program entries requires low-level
manipulation that does break the abstraction over `proof_entry`; we
thus introduce `prepare_obligation`, and move the code that prepares
the obligation entry to its own module.

This seems to improve separation of concerns, and helps clarify the
two of three current models in which Coq operates w.r.t. definitions:

- single, ground entries with possibly mutual definitions [regular lemmas]
- single, non-ground entries with possibly mutual definitions [obligations]
- multiple entries [equations]
---
 vernac/declareDef.ml | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index b0c8fe90c4..f283f700b7 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -157,7 +157,8 @@ let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
   if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
 
-let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+  let allow_evars = false in
   check_definition_evars ~allow_evars sigma;
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
       sigma (fun nf -> nf body, Option.map nf types)
@@ -165,6 +166,28 @@ let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body si
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, definition_entry ?opaque ?inline ?types ~univs body
 
+let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
+  let allow_evars = true in
+  check_definition_evars ~allow_evars sigma;
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+      sigma (fun nf -> nf body, Option.map nf types)
+  in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let ce = definition_entry ?opaque ?inline ?types ~univs body in
+  let env = Global.env () in
+  let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
+  assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
+  assert(Univ.ContextSet.is_empty ctx);
+  RetrieveObl.check_evars env sigma;
+  let c = EConstr.of_constr c in
+  let typ = match ce.Declare.proof_entry_type with
+    | Some t -> EConstr.of_constr t
+    | None -> Retyping.get_type_of env sigma c
+  in
+  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
+  let uctx = Evd.evar_universe_context sigma in
+  c, cty, uctx, obls
+
 let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma =
   check_definition_evars ~allow_evars sigma;
   let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
-- 
cgit v1.2.3


From d507679b5b6dfac944e038b6a3ebd9fb8e6998ff Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 03:19:15 -0400
Subject: [declareDef] Cleanup of allow_evars and check_evars

We don't the parameter anymore as the paths are too different now.

Note that this removes a duplicate `check_evars` that has been in
`master` quite some time [double check in `ComDefinition` and in
`DeclareDef.prepare_definition`]
---
 vernac/declareDef.ml | 21 ++++++++-------------
 1 file changed, 8 insertions(+), 13 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index f283f700b7..2528dfd38f 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -153,23 +153,17 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
 
 (* Preparing proof entries *)
 
-let check_definition_evars ~allow_evars sigma =
-  let env = Global.env () in
-  if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
-
 let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
-  let allow_evars = false in
-  check_definition_evars ~allow_evars sigma;
-  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+  let env = Global.env () in
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, definition_entry ?opaque ?inline ?types ~univs body
 
 let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
-  let allow_evars = true in
-  check_definition_evars ~allow_evars sigma;
-  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
@@ -188,9 +182,10 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let uctx = Evd.evar_universe_context sigma in
   c, cty, uctx, obls
 
-let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma =
-  check_definition_evars ~allow_evars sigma;
-  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+let prepare_parameter ~poly ~udecl ~types sigma =
+  let env = Global.env () in
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true
       sigma (fun nf -> nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-- 
cgit v1.2.3


From 8ac27a8261f5f3fb5d4bf2a207a144df07477910 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 03:42:57 -0400
Subject: [declare] Make the type of closed entries opaque.

This is a step in forcing all entry creation go thru the preparation
functions. We still need to handle plain `Declare.` calls, but this
will be next step.

We need to leave a backdoor for interactive proofs until we unify
proof preparation happening in `Proof_global` with the one happening
in `DeclareDef`, but we are getting there.

TODO: see how to avoid the normalization problems in DeclareObl
---
 vernac/declareDef.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 2528dfd38f..84310cba65 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -38,6 +38,13 @@ module Hook = struct
 
 end
 
+module ClosedDef = struct
+
+  type t = Evd.side_effects Declare.proof_entry
+
+  let of_proof_entry x = x
+end
+
 (* Locality stuff *)
 let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   let should_suggest = ce.Declare.proof_entry_opaque &&
@@ -153,14 +160,14 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
 
 (* Preparing proof entries *)
 
-let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma =
   let env = Global.env () in
   Pretyping.check_evars_are_solved ~program_mode:false env sigma;
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  sigma, definition_entry ?opaque ?inline ?types ~univs body
+  sigma, definition_entry ?fix_exn ?opaque ?inline ?types ~univs body
 
 let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
-- 
cgit v1.2.3


From 8fbc927ac40cc707b1a940d8339a2a289755d533 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 16:34:30 -0400
Subject: [declareDef] More consistent handling of universe binders

The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook

We handle this automatically now; it seems like a reasonably good API
improvement.

However, it is not clear what we do now is right for all cases; must
check.
---
 vernac/declareDef.ml | 54 ++++++++++++++++++++++++++--------------------------
 1 file changed, 27 insertions(+), 27 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 84310cba65..14d3daf453 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Declare
-open Impargs
 
 type locality = Discharge | Global of Declare.import_status
 
@@ -40,40 +39,40 @@ end
 
 module ClosedDef = struct
 
-  type t = Evd.side_effects Declare.proof_entry
+  type t =
+    { entry : Evd.side_effects Declare.proof_entry
+    ; uctx : UState.t
+    }
 
-  let of_proof_entry x = x
+  let of_proof_entry ~uctx entry = { entry; uctx }
 end
 
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
-  let should_suggest = ce.Declare.proof_entry_opaque &&
-                       Option.is_empty ce.Declare.proof_entry_secctx in
+let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce =
+  let { ClosedDef.entry; uctx } = ce in
+  let should_suggest = entry.Declare.proof_entry_opaque &&
+                       Option.is_empty entry.Declare.proof_entry_secctx in
+  let ubind = UState.universe_binders uctx in
   let dref = match scope with
   | Discharge ->
-    let () = declare_variable ~name ~kind (SectionLocalDef ce) in
+    let () = declare_variable ~name ~kind (SectionLocalDef entry) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
   | Global local ->
-    let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
+    let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
     let () = DeclareUniv.declare_univ_binders gr ubind in
     gr
   in
-  let () = maybe_declare_manual_implicits false dref impargs in
+  let () = Impargs.maybe_declare_manual_implicits false dref impargs in
   let () = definition_message name in
-  begin
-    match hook_data with
-    | None -> ()
-    | Some (hook, uctx, obls) ->
-      Hook.call ~hook { Hook.S.uctx; obls; scope; dref }
-  end;
+  Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
   dref
 
-let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
-  let fix_exn = Declare.Internal.get_fix_exn ce in
-  try declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce
+let declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce =
+  let fix_exn = Declare.Internal.get_fix_exn ce.ClosedDef.entry in
+  try declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce
   with exn ->
     let exn = Exninfo.capture exn in
     Exninfo.iraise (fix_exn exn)
@@ -107,22 +106,21 @@ end
 let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
   let vars, fixdecls, indexes =
     mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
-  let ubind, univs =
+  let uctx, univs =
     (* XXX: Obligations don't do this, this seems like a bug? *)
     if restrict_ucontext
     then
-      let evd = Evd.from_ctx uctx in
-      let evd = Evd.restrict_universe_context evd vars in
-      let univs = Evd.check_univ_decl ~poly evd udecl in
-      Evd.universe_binders evd, univs
+      let uctx = UState.restrict uctx vars in
+      let univs = UState.check_univ_decl ~poly uctx udecl in
+      uctx, univs
     else
       let univs = UState.univ_entry ~poly uctx in
-      UnivNames.empty_binders, univs
+      uctx, univs
   in
   let csts = CList.map2
       (fun Recthm.{ name; typ; impargs } body ->
-         let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in
-         declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+         let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in
+         declare_definition ~name ~scope ~kind ~impargs { ClosedDef.entry; uctx })
       fixitems fixdecls
   in
   let isfix = Option.is_empty possible_indexes in
@@ -167,7 +165,9 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  sigma, definition_entry ?fix_exn ?opaque ?inline ?types ~univs body
+  let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
+  let uctx = Evd.evar_universe_context sigma in
+  { ClosedDef.entry; uctx }
 
 let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
-- 
cgit v1.2.3


From 7d46a32dc928af64e3e111d6d62caa00f93c427c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 18 Mar 2020 05:35:41 -0400
Subject: [declare] Fuse prepare and declare for the non-interactive path.

This will allow to share the definition metadata for example with
obligations; a bit more work is needed to finally move the preparation
of interactive proofs from Proof_global to `prepare_entry`.
---
 vernac/declareDef.ml | 28 +++++++++++-----------------
 1 file changed, 11 insertions(+), 17 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 14d3daf453..356e8f091e 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -37,19 +37,8 @@ module Hook = struct
 
 end
 
-module ClosedDef = struct
-
-  type t =
-    { entry : Evd.side_effects Declare.proof_entry
-    ; uctx : UState.t
-    }
-
-  let of_proof_entry ~uctx entry = { entry; uctx }
-end
-
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce =
-  let { ClosedDef.entry; uctx } = ce in
+let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
   let should_suggest = entry.Declare.proof_entry_opaque &&
                        Option.is_empty entry.Declare.proof_entry_secctx in
   let ubind = UState.universe_binders uctx in
@@ -70,9 +59,9 @@ let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce =
   Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
   dref
 
-let declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce =
-  let fix_exn = Declare.Internal.get_fix_exn ce.ClosedDef.entry in
-  try declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce
+let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry =
+  let fix_exn = Declare.Internal.get_fix_exn entry in
+  try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry
   with exn ->
     let exn = Exninfo.capture exn in
     Exninfo.iraise (fix_exn exn)
@@ -120,7 +109,7 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
   let csts = CList.map2
       (fun Recthm.{ name; typ; impargs } body ->
          let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in
-         declare_definition ~name ~scope ~kind ~impargs { ClosedDef.entry; uctx })
+         declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
       fixitems fixdecls
   in
   let isfix = Option.is_empty possible_indexes in
@@ -167,7 +156,12 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
   let uctx = Evd.evar_universe_context sigma in
-  { ClosedDef.entry; uctx }
+  entry, uctx
+
+let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
+    ?obls ~poly ?inline ~types ~body ?fix_exn sigma =
+  let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
+  declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
 
 let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
-- 
cgit v1.2.3


From 1320d5004b58f33c2274bfdc0629d7f513cd49c4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 30 Mar 2020 15:02:50 -0400
Subject: [declare] [nit] Get `fix_exn` only in the case of an exception.

Suggested by Gaëtan Gilbert.
---
 vernac/declareDef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 356e8f091e..1607771598 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -60,10 +60,10 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
   dref
 
 let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry =
-  let fix_exn = Declare.Internal.get_fix_exn entry in
   try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry
   with exn ->
     let exn = Exninfo.capture exn in
+    let fix_exn = Declare.Internal.get_fix_exn entry in
     Exninfo.iraise (fix_exn exn)
 
 let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
-- 
cgit v1.2.3