From 763990af5a28ca7b1fa77bc763c878b23fd93f8c Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 17:14:58 -0400
Subject: [PATCH 01/42] Port plibrary.ml4 to mlg

---
 _CoqProject                        | 2 +-
 src/{plibrary.ml4 => plibrary.mlg} | 0
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename src/{plibrary.ml4 => plibrary.mlg} (100%)

diff --git a/_CoqProject b/_CoqProject
index 339b268..2edf0c1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -91,7 +91,7 @@ src/coq/devutils/printing.ml
 src/coq/decompiler/decompiler.mli
 src/coq/decompiler/decompiler.ml
 
-src/plibrary.ml4
+src/plibrary.mlg
 src/plib.mlpack
 
 theories/Plib.v
diff --git a/src/plibrary.ml4 b/src/plibrary.mlg
similarity index 100%
rename from src/plibrary.ml4
rename to src/plibrary.mlg

From cf1ab439741d945d02f91288935794395046cf2e Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 17:32:42 -0400
Subject: [PATCH 02/42] Add missing cases to map3

---
 src/utilities/utilities.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/utilities/utilities.ml b/src/utilities/utilities.ml
index 2d54096..3cff55b 100644
--- a/src/utilities/utilities.ml
+++ b/src/utilities/utilities.ml
@@ -138,7 +138,11 @@ let combine_cartesian_append (al : 'a list array) : 'a array list =
 (* Map3 *)
 let rec map3 (f : 'a -> 'b -> 'c -> 'd) l1 l2 l3 : 'd list =
   match (l1, l2, l3) with
-  | ([], [], []) ->
+  | ([], _, _) ->
+     []
+  | (_, [], _) ->
+     []
+  | (_, _, []) ->
      []
   | (h1 :: t1, h2 :: t2, h3 :: t3) ->
      let r = f h1 h2 h3 in r :: map3 f t1 t2 t3

From 5ebea67694275388f71c97aa84af390cd1013039 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 17:33:18 -0400
Subject: [PATCH 03/42] Update Global.body_of_constant call to reflect changes
 in Coq impl

---
 src/coq/termutils/constutils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq/termutils/constutils.ml b/src/coq/termutils/constutils.ml
index 4a8e384..27bd38f 100644
--- a/src/coq/termutils/constutils.ml
+++ b/src/coq/termutils/constutils.ml
@@ -18,7 +18,7 @@ let make_constant id =
  * Safely extract the body of a constant, instantiating any universe variables 
  *)
 let open_constant env const =
-  let (Some (term, auctx)) = Global.body_of_constant const in
+  let (Some (term, _, auctx)) = Global.body_of_constant Library.indirect_accessor const in
   let uctx = Universes.fresh_instance_from_context auctx |> Univ.UContext.make in
   let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in
   let env = Environ.push_context uctx env in

From 3ab41c82aebbd8777195ccf4cf3b3d3b62ce399e Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 18:00:22 -0400
Subject: [PATCH 04/42] Port to 8.10; handle all cases; remove unused Environ

---
 src/coq/termutils/constutils.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/coq/termutils/constutils.ml b/src/coq/termutils/constutils.ml
index 27bd38f..9886f2d 100644
--- a/src/coq/termutils/constutils.ml
+++ b/src/coq/termutils/constutils.ml
@@ -3,7 +3,6 @@
  *)
 
 open Constr
-open Environ
 open Names
 
 (* --- Constructing constants --- *)
@@ -18,8 +17,10 @@ let make_constant id =
  * Safely extract the body of a constant, instantiating any universe variables 
  *)
 let open_constant env const =
-  let (Some (term, _, auctx)) = Global.body_of_constant Library.indirect_accessor const in
-  let uctx = Universes.fresh_instance_from_context auctx |> Univ.UContext.make in
-  let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in
-  let env = Environ.push_context uctx env in
-  env, term
+  match Global.body_of_constant Library.indirect_accessor const with 
+    | (Some (term, _, auctx)) -> 
+      let (uinst, uctxset) = UnivGen.fresh_instance auctx in 
+      let uctx = Univ.UContext.make (uinst, (Univ.ContextSet.constraints uctxset)) in
+      let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in
+      let env = Environ.push_context uctx env in env, term
+    | None -> failwith "Constant extraction failed"

From d9f5ca6d8436cc01af34b362f4852b1df0a3536b Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 18:07:47 -0400
Subject: [PATCH 05/42] Fail loudly in map3 if args have mismatched size

---
 src/utilities/utilities.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/utilities/utilities.ml b/src/utilities/utilities.ml
index 3cff55b..5bff4bc 100644
--- a/src/utilities/utilities.ml
+++ b/src/utilities/utilities.ml
@@ -138,12 +138,11 @@ let combine_cartesian_append (al : 'a list array) : 'a array list =
 (* Map3 *)
 let rec map3 (f : 'a -> 'b -> 'c -> 'd) l1 l2 l3 : 'd list =
   match (l1, l2, l3) with
-  | ([], _, _) ->
-     []
-  | (_, [], _) ->
-     []
-  | (_, _, []) ->
+  | ([], [], []) ->
      []
+  | ([], _, _) -> failwith "Mismatched sized lists passed to map3"
+  | (_, [], _) -> failwith "Mismatched sized lists passed to map3"
+  | (_, _, []) -> failwith "Mismatched sized lists passed to map3"
   | (h1 :: t1, h2 :: t2, h3 :: t3) ->
      let r = f h1 h2 h3 in r :: map3 f t1 t2 t3
 

From 7ede24ecbe46c7d34c584667fa7b41af05df71f2 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 18:20:36 -0400
Subject: [PATCH 06/42] Add Globnames to scope

---
 src/coq/representationutils/defutils.mli | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/coq/representationutils/defutils.mli b/src/coq/representationutils/defutils.mli
index 84cfc2e..1035648 100644
--- a/src/coq/representationutils/defutils.mli
+++ b/src/coq/representationutils/defutils.mli
@@ -7,6 +7,7 @@ open Names
 open Evd
 open Environ
 open Constrexpr
+open Globnames
 
 (* --- Defining Coq terms --- *)
 

From a3dd7f91574942004f8a6f98ffd62d3f6c617a61 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 20:05:57 -0400
Subject: [PATCH 07/42] Port defutils to Coq 8.11; whew!

---
 src/coq/representationutils/defutils.ml | 52 ++++++++++++-------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml
index a18b343..e683f10 100644
--- a/src/coq/representationutils/defutils.ml
+++ b/src/coq/representationutils/defutils.ml
@@ -2,11 +2,8 @@
  * Utilities for defining terms
  *)
 
-open Constr
 open Names
 open Evd
-open Decl_kinds
-open Recordops
 open Constrexpr
 open Constrextern
 
@@ -15,7 +12,7 @@ open Constrextern
 (* https://github.com/ybertot/plugin_tutorials/blob/master/tuto1/src/simple_declare.ml 
 
 TODO do we need to return the updated evar_map? *)
-let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook refresh =
+let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh =
   let open EConstr in
   (* XXX: "Standard" term construction combinators such as `mkApp`
      don't add any universe constraints that may be needed later for
@@ -56,25 +53,27 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook re
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   let ubinders = Evd.universe_binders sigma in
   let ce = Declare.definition_entry ?types:tyopt ~univs body in
-  DeclareDef.declare_definition ident k ce ubinders imps hook
+  DeclareDef.declare_definition ~name:ident ~scope:(Locality.enforce_locality_exp None Vernacexpr.NoDischarge) ~kind:(Decls.variable_kind ident) ?hook_data:hook ubinders ce imps (* todo: does this even work? *)
 
 (* Define a new Coq term *)
-let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) =
-  let k = (Global, Flags.is_universe_polymorphism(), Definition) in
+let define_term ?typ (n : Id.t) (evm : evar_map) (trm : Constr.types) (refresh : bool) =
+  (* let k = (Global, Flags.is_universe_polymorphism(), Definition) in *)
+  let poly = Attributes.is_universe_polymorphism() in
   let udecl = UState.default_univ_decl in
-  let nohook = Lemmas.mk_hook (fun _ x -> x) in
+  (* let nohook = Lemmas.mk_hook (fun _ x -> x) in *)
   let etrm = EConstr.of_constr trm in
   let etyp = Option.map EConstr.of_constr typ in
-  edeclare n k ~opaque:false evm udecl etrm etyp [] nohook refresh
+  edeclare n poly ~opaque:false evm udecl etrm etyp [] None refresh
 
 (* Define a Canonical Structure *)
-let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) =
-  let k = (Global, Flags.is_universe_polymorphism (), CanonicalStructure) in
+let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : Constr.types) (refresh : bool) =
+  (* let k = (Global, Flags.is_universe_polymorphism(), Definition) in *)
+  let poly = Attributes.is_universe_polymorphism() in
   let udecl = UState.default_univ_decl in
-  let hook = Lemmas.mk_hook (fun _ x -> declare_canonical_structure x; x) in
+  let hook = DeclareDef.Hook.make (fun x -> let open DeclareDef.Hook.S in Canonical.declare_canonical_structure x.dref) in
   let etrm = EConstr.of_constr trm in
   let etyp = Option.map EConstr.of_constr typ in
-  edeclare n k ~opaque:false evm udecl etrm etyp [] hook refresh
+  edeclare n poly ~opaque:false evm udecl etrm etyp [] (Some (hook, Evd.evar_universe_context evm, [])) refresh (* todo: check if last empty list is correct to pass *)
 
 (* --- Converting between representations --- *)
 
@@ -83,7 +82,7 @@ let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : b
  *)
 
 (* Intern a term (for now, ignore the resulting evar_map) *)
-let intern env sigma t : evar_map * types =
+let intern env sigma t : evar_map * Constr.types =
   let (sigma, trm) = Constrintern.interp_constr_evars env sigma t in
   sigma, EConstr.to_constr sigma trm
 
@@ -92,30 +91,31 @@ let extern env sigma t : constr_expr =
   Constrextern.extern_constr true env sigma (EConstr.of_constr t)
 
 (* Construct the external expression for a definition *)
-let expr_of_global (g : global_reference) : constr_expr =
+let expr_of_global (g : Globnames.global_reference) : constr_expr =
   let r = extern_reference Id.Set.empty g in
   CAst.make @@ (CAppExpl ((None, r, None), []))
 
 (* Convert a term into a global reference with universes (or raise Not_found) *)
 let pglobal_of_constr term =
-  match Constr.kind term with
-  | Const (const, univs) -> Globnames.ConstRef const, univs
-  | Ind (ind, univs) -> IndRef ind, univs
-  | Construct (cons, univs) -> ConstructRef cons, univs
-  | Var id -> VarRef id, Univ.Instance.empty
-  | _ -> raise Not_found
+  let open Constr in 
+    match Constr.kind term with
+    | Const (const, univs) -> Globnames.ConstRef const, univs
+    | Ind (ind, univs) ->  Names.GlobRef.IndRef ind, univs
+    | Construct (cons, univs) -> Names.GlobRef.ConstructRef cons, univs
+    | Var id -> Names.GlobRef.VarRef id, Univ.Instance.empty
+    | _ -> raise Not_found
 
 (* Convert a global reference with universes into a term *)
 let constr_of_pglobal (glob, univs) =
   match glob with
-  | Globnames.ConstRef const -> mkConstU (const, univs)
-  | IndRef ind -> mkIndU (ind, univs)
-  | ConstructRef cons -> mkConstructU (cons, univs)
-  | VarRef id -> mkVar id
+  | Globnames.ConstRef const -> Constr.mkConstU (const, univs)
+  | Names.GlobRef.IndRef ind -> Constr.mkIndU (ind, univs)
+  | Names.GlobRef.ConstructRef cons -> Constr.mkConstructU (cons, univs)
+  | Names.GlobRef.VarRef id -> Constr.mkVar id
 
 (* Safely instantiate a global reference, with proper universe handling *)
 let new_global sigma gref =
   let sigma_ref = ref sigma in
-  let glob =  Evarutil.e_new_global sigma_ref gref in
+  let (_, glob) = Evarutil.new_global sigma gref in
   let sigma = ! sigma_ref in
   sigma, EConstr.to_constr sigma glob

From ad7c8e6ed7b6abbcfbb10166ac4afac74b473b7c Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 20:06:29 -0400
Subject: [PATCH 08/42] Remove unused import from nameutils

---
 src/coq/representationutils/nameutils.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/coq/representationutils/nameutils.ml b/src/coq/representationutils/nameutils.ml
index 9432148..cf72370 100644
--- a/src/coq/representationutils/nameutils.ml
+++ b/src/coq/representationutils/nameutils.ml
@@ -2,7 +2,6 @@
  * Utilities for names, references, and identifiers
  *)
 
-open Constr
 open Names
 open Util
 

From f90d9faf07263a9aa80fbcd043fcb3909f6bb2f4 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 20:14:07 -0400
Subject: [PATCH 09/42] Port inference.ml to 8.11; remove unused imports

See: https://github.com/coq/coq/blame/master/doc/sphinx/changes.rst#L8195
---
 src/coq/logicutils/typesandequality/inference.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/src/coq/logicutils/typesandequality/inference.ml b/src/coq/logicutils/typesandequality/inference.ml
index 31af8fe..f01f546 100644
--- a/src/coq/logicutils/typesandequality/inference.ml
+++ b/src/coq/logicutils/typesandequality/inference.ml
@@ -2,25 +2,19 @@
  * Type inference
  *)
 
-open Environ
-open Evd
 open Constr
 open Declarations
              
 (* Safely infer the WHNF type of a term, updating the evar map *)
 let infer_type env sigma term =
-  let sigma_ref = ref sigma in
   let eterm = EConstr.of_constr term in
-  let typ = Typing.e_type_of ~refresh:true env sigma_ref eterm in
-  let sigma = ! sigma_ref in
+  let (sigma, typ) = Typing.type_of ~refresh:true env sigma eterm in
   sigma, EConstr.to_constr sigma typ
 
 (* Safely infer the sort of a type, updating the evar map *)
 let infer_sort env sigma term =
-  let sigma_ref = ref sigma in
   let eterm = EConstr.of_constr term in
-  let sort = Typing.e_sort_of env sigma_ref eterm in
-  let sigma = ! sigma_ref in
+  let (sigma, sort) = Typing.sort_of env sigma eterm in
   sigma, Sorts.family sort
 
 (* Get the type of an inductive type (TODO do we need evar_map here?) *)

From bad58f6dedc01d57685f5778d73707c1e9202d3d Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 22:27:15 -0400
Subject: [PATCH 10/42] Finish porting over contextutils.ml (breaking change!)

Note: this introduces a breaking change with the type signatures of one of the
helper functions . . .
---
 src/coq/logicutils/contexts/contextutils.ml  | 65 ++++++++++++--------
 src/coq/logicutils/contexts/contextutils.mli | 13 ++++
 2 files changed, 53 insertions(+), 25 deletions(-)

diff --git a/src/coq/logicutils/contexts/contextutils.ml b/src/coq/logicutils/contexts/contextutils.ml
index d44c7cc..104089d 100644
--- a/src/coq/logicutils/contexts/contextutils.ml
+++ b/src/coq/logicutils/contexts/contextutils.ml
@@ -13,20 +13,6 @@ open Declarations
 
 module CRD = Context.Rel.Declaration
 module CND = Context.Named.Declaration
-
-(* --- Questions about declarations --- *)
-
-(* Is the rel declaration a local assumption? *)
-let is_rel_assum = CRD.is_local_assum
-
-(* Is the rel declaration a local definition? *)
-let is_rel_defin = CRD.is_local_def
-
-(* Is the named declaration an assumption? *)
-let is_named_assum = CND.is_local_assum
-
-(* Is the named declaration a definition? *)
-let is_named_defin = CND.is_local_def
                        
 (* --- Deconstructing declarations --- *)
 
@@ -47,14 +33,40 @@ let named_value decl = CND.get_value decl
 
 (* Get the type of a named declaration *)
 let named_type decl = CND.get_type decl
+
+(* --- Questions about declarations --- *)
+
+(* Is the rel declaration a local assumption? *)
+let is_rel_assum = CRD.is_local_assum
+
+(* Is the rel declaration a local definition? *)
+(* let is_rel_defin x = CRD.is_local_def (get_rel_ctx_name x) *)
+let is_rel_defin x = CRD.is_local_def x
+
+(* Is the named declaration an assumption? *)
+let is_named_assum = CND.is_local_assum
+
+(* Is the named declaration a definition? *)
+let is_named_defin = CND.is_local_def
     
+(* --- Context manipulation tools --- *)
+
+(* Get relative context for a name *)
+let get_rel_ctx_name name = 
+  match name with (* handle if anon or not *)
+  | Anonymous -> Context.anonR
+  | Name idt -> Context.nameR idt
+
+(* Get relative context for a declaration *)
+let get_rel_ctx decl = get_rel_ctx_name (rel_name decl)
+
 (* --- Constructing declarations --- *)
 
 (* Make the rel declaration for a local assumption *)
-let rel_assum (name, typ) = CRD.LocalAssum (name, typ)
+let rel_assum (name, typ) = CRD.LocalAssum (get_rel_ctx_name name, typ)
 
 (* Make the rel declaration for a local definition *)
-let rel_defin (name, def, typ) = CRD.LocalDef (name, def, typ)
+let rel_defin (name, def, typ) = CRD.LocalDef (get_rel_ctx_name name, def, typ)
 
 (* Make the named declaration for a local assumption *)
 let named_assum (id, typ) = CND.LocalAssum (id, typ)
@@ -104,7 +116,7 @@ let smash_prod_assum ctxt body =
     (fun body decl ->
        match rel_value decl with
        | Some defn -> Vars.subst1 defn body
-       | None -> mkProd (rel_name decl, rel_type decl, body))
+       | None -> mkProd (get_rel_ctx decl, rel_type decl, body))
     ~init:body
     ctxt
 
@@ -117,7 +129,7 @@ let smash_lam_assum ctxt body =
     (fun body decl ->
        match rel_value decl with
        | Some defn -> Vars.subst1 defn body
-       | None -> mkLambda (rel_name decl, rel_type decl, body))
+       | None -> mkLambda (get_rel_ctx decl, rel_type decl, body))
     ~init:body
     ctxt
 
@@ -127,11 +139,12 @@ let smash_lam_assum ctxt body =
  *)
 let decompose_prod_n_zeta n term =
   assert (n >= 0);
+  let open Context in
   let rec aux n ctxt body =
     if n > 0 then
       match Constr.kind body with
       | Prod (name, param, body) ->
-        aux (n - 1) (Context.Rel.add (rel_assum (name, param)) ctxt) body
+        aux (n - 1) (Rel.add (rel_assum (name.binder_name, param)) ctxt) body
       | LetIn (name, def_term, def_type, body) ->
         aux n ctxt (Vars.subst1 def_term body)
       | _ ->
@@ -139,7 +152,7 @@ let decompose_prod_n_zeta n term =
     else
       ctxt, body
   in
-  aux n Context.Rel.empty term
+  aux n Rel.empty term
 
 (*
  * Decompose the first n lambda bindings, zeta-reducing let bindings to reveal
@@ -147,11 +160,12 @@ let decompose_prod_n_zeta n term =
  *)
 let decompose_lam_n_zeta n term =
   assert (n >= 0);
+  let open Context in
   let rec aux n ctxt body =
     if n > 0 then
       match Constr.kind body with
       | Lambda (name, param, body) ->
-        aux (n - 1) (Context.Rel.add (rel_assum (name, param)) ctxt) body
+        aux (n - 1) (Rel.add (rel_assum (name.binder_name, param)) ctxt) body
       | LetIn (name, def_term, def_type, body) ->
         Vars.subst1 def_term body |> aux n ctxt
       | _ ->
@@ -159,7 +173,7 @@ let decompose_lam_n_zeta n term =
     else
       ctxt, body
   in
-  aux n Context.Rel.empty term
+  aux n Rel.empty term
 
 (* Bind the declarations of a local context as product/let-in bindings *)
 let recompose_prod_assum decls term =
@@ -200,8 +214,8 @@ let bindings_for_inductive env mutind_body ind_bodies : rel_declaration list =
        (fun i ind_body ->
          let name_id = ind_body.mind_typename in
          let typ = type_of_inductive env i mutind_body in
-         CRD.LocalAssum (Name name_id, typ))
-       ind_bodies)
+         CRD.LocalAssum (Context.nameR name_id, typ))
+       mutind_body.mind_packets)
 
 (*
  * Fixpoints
@@ -210,7 +224,8 @@ let bindings_for_fix (names : name array) (typs : types array) : rel_declaration
   Array.to_list
     (CArray.map2_i
        (fun i name typ -> CRD.LocalAssum (name, Vars.lift i typ))
-       names typs)
+       (Array.map get_rel_ctx_name names)
+       typs)
 
 (* --- Combining contexts --- *)
 
diff --git a/src/coq/logicutils/contexts/contextutils.mli b/src/coq/logicutils/contexts/contextutils.mli
index f227051..739773c 100644
--- a/src/coq/logicutils/contexts/contextutils.mli
+++ b/src/coq/logicutils/contexts/contextutils.mli
@@ -35,8 +35,21 @@ val define_rel_decl :
 (*
  * Construct a named assumption/definition
  *)
+val named_assum : Id.t Context.binder_annot * 'types -> ('constr, 'types) CND.pt
+val named_defin : Id.t Context.binder_annot * 'constr * 'types -> ('constr, 'types) CND.pt
+
+(* Old version, breaking change. TODO: make sure this doesn't affect any downstream plugins
 val named_assum : Id.t * 'types -> ('constr, 'types) CND.pt
 val named_defin : Id.t * 'constr * 'types -> ('constr, 'types) CND.pt
+*)
+
+(* Context name/decl manipulation *)
+(*
+TODO: fill out
+val get_rel_ctx_name : Names.name -> Names.Name.t Context.binder_annot
+
+val get_rel_ctx : ('constr, 'types) CND.pt -> Names.Name.t Context.binder_annot
+*)
 
 (* --- Questions about declarations --- *)
 

From c69de0d8631cab780bd6ceceb640867fab1507d0 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 23:07:54 -0400
Subject: [PATCH 11/42] Turn "pattern-matching is not exhaustive" warnings back
 to warnings

---
 Makefile.local | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 Makefile.local

diff --git a/Makefile.local b/Makefile.local
new file mode 100644
index 0000000..3dbf942
--- /dev/null
+++ b/Makefile.local
@@ -0,0 +1 @@
+OCAMLWARN=-warn-error +a-3-8

From 0fcf2c86d61daaa5d836baf49cc75f12003fc154 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 23:09:14 -0400
Subject: [PATCH 12/42] Remove unused import

---
 src/coq/logicutils/typesandequality/convertibility.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/coq/logicutils/typesandequality/convertibility.ml b/src/coq/logicutils/typesandequality/convertibility.ml
index 8b1a854..c50b46e 100644
--- a/src/coq/logicutils/typesandequality/convertibility.ml
+++ b/src/coq/logicutils/typesandequality/convertibility.ml
@@ -4,7 +4,6 @@
 
 open Constr
 open Contextutils
-open Utilities
 open Environ
 open Evd
 open Inference

From 827ea2f703cba0652f6d3873b4ac9a74736a7156 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 23:11:42 -0400
Subject: [PATCH 13/42] Remove unused import

---
 src/coq/constants/idutils.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/coq/constants/idutils.ml b/src/coq/constants/idutils.ml
index 8bf2da7..1f109d8 100644
--- a/src/coq/constants/idutils.ml
+++ b/src/coq/constants/idutils.ml
@@ -4,7 +4,6 @@
 
 open Constr
 open Names
-open Environ
 open Evd
 
 let coq_init_datatypes =

From 5e92a935d652f6ac398c8f513e8ecbcfe6538531 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 23:13:05 -0400
Subject: [PATCH 14/42] Add necessary import

---
 src/coq/constants/idutils.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/coq/constants/idutils.ml b/src/coq/constants/idutils.ml
index 1f109d8..718ed88 100644
--- a/src/coq/constants/idutils.ml
+++ b/src/coq/constants/idutils.ml
@@ -5,6 +5,7 @@
 open Constr
 open Names
 open Evd
+open Sorts
 
 let coq_init_datatypes =
   ModPath.MPfile

From 6f7a0ddf6829cc43fcfba921692c68c4d08ff952 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 23:15:05 -0400
Subject: [PATCH 15/42] Add warning 40 to not fatal list of warnings

---
 Makefile.local               | 2 +-
 src/coq/constants/idutils.ml | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/Makefile.local b/Makefile.local
index 3dbf942..ec5478e 100644
--- a/Makefile.local
+++ b/Makefile.local
@@ -1 +1 @@
-OCAMLWARN=-warn-error +a-3-8
+OCAMLWARN=-warn-error +a-3-8-40
diff --git a/src/coq/constants/idutils.ml b/src/coq/constants/idutils.ml
index 718ed88..1f109d8 100644
--- a/src/coq/constants/idutils.ml
+++ b/src/coq/constants/idutils.ml
@@ -5,7 +5,6 @@
 open Constr
 open Names
 open Evd
-open Sorts
 
 let coq_init_datatypes =
   ModPath.MPfile

From 391a7d7677c9548f4e51710e16a3b57092e1fe71 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 2 Aug 2022 23:17:04 -0400
Subject: [PATCH 16/42] Update KerName.make2 calls to Names.KerName.make

---
 src/coq/constants/equtils.ml    | 2 +-
 src/coq/constants/produtils.ml  | 2 +-
 src/coq/constants/proputils.ml  | 5 ++---
 src/coq/constants/sigmautils.ml | 2 +-
 src/plibrary.ml                 | 2 ++
 5 files changed, 7 insertions(+), 6 deletions(-)
 create mode 100644 src/plibrary.ml

diff --git a/src/coq/constants/equtils.ml b/src/coq/constants/equtils.ml
index a1ed2a8..323c1a4 100644
--- a/src/coq/constants/equtils.ml
+++ b/src/coq/constants/equtils.ml
@@ -14,7 +14,7 @@ let coq_init_logic =
 
 (* equality *)
 let eq : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "eq")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "eq")), 0)
 
 (* Constructor for quality *)
 let eq_refl : types =
diff --git a/src/coq/constants/produtils.ml b/src/coq/constants/produtils.ml
index a07adbe..f3942d3 100644
--- a/src/coq/constants/produtils.ml
+++ b/src/coq/constants/produtils.ml
@@ -14,7 +14,7 @@ let coq_init_data =
 
 (* prod types *)
 let prod : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_data (Label.make "prod")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_data (Label.make "prod")), 0)
 
 (* Introduction for sigma types *)
 let pair : constr =
diff --git a/src/coq/constants/proputils.ml b/src/coq/constants/proputils.ml
index ecc32b1..3af7aeb 100644
--- a/src/coq/constants/proputils.ml
+++ b/src/coq/constants/proputils.ml
@@ -4,7 +4,6 @@
 
 open Constr
 open Names
-open Apputils
 
 let coq_init_logic =
   ModPath.MPfile
@@ -14,7 +13,7 @@ let coq_init_logic =
 
 (* Logical or *)
 let logical_or : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "or")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "or")), 0)
   
 (* left constructor of \/ *)
 let or_introl : types =
@@ -27,7 +26,7 @@ let or_intror : types =
 
 (* Logical and *)
 let logical_and : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "and")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "and")), 0)
   
 (* constructor of /\ *)
 let conj : types =
diff --git a/src/coq/constants/sigmautils.ml b/src/coq/constants/sigmautils.ml
index a7ed555..b92acf9 100644
--- a/src/coq/constants/sigmautils.ml
+++ b/src/coq/constants/sigmautils.ml
@@ -14,7 +14,7 @@ let coq_init_specif =
 
 (* sigma types *)
 let sigT : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_specif (Label.make "sigT")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_specif (Label.make "sigT")), 0)
 
 (* Introduction for sigma types *)
 let existT : types =
diff --git a/src/plibrary.ml b/src/plibrary.ml
new file mode 100644
index 0000000..9993ab4
--- /dev/null
+++ b/src/plibrary.ml
@@ -0,0 +1,2 @@
+let __coq_plugin_name = "plib"
+let _ = Mltop.add_known_module __coq_plugin_name

From ba601ddfbb3a76d2f2e361a0ead2e29ec39db1e9 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Wed, 3 Aug 2022 21:46:04 -0400
Subject: [PATCH 17/42] Finish porting substitution.ml to 8.11 (breaking
 change!)

---
 src/coq/logicutils/contexts/contextutils.mli | 5 +----
 src/coq/logicutils/hofs/substitution.ml      | 4 ++--
 src/coq/logicutils/hofs/substitution.mli     | 3 +--
 3 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/coq/logicutils/contexts/contextutils.mli b/src/coq/logicutils/contexts/contextutils.mli
index 739773c..9faf1c6 100644
--- a/src/coq/logicutils/contexts/contextutils.mli
+++ b/src/coq/logicutils/contexts/contextutils.mli
@@ -44,12 +44,9 @@ val named_defin : Id.t * 'constr * 'types -> ('constr, 'types) CND.pt
 *)
 
 (* Context name/decl manipulation *)
-(*
-TODO: fill out
 val get_rel_ctx_name : Names.name -> Names.Name.t Context.binder_annot
 
-val get_rel_ctx : ('constr, 'types) CND.pt -> Names.Name.t Context.binder_annot
-*)
+val get_rel_ctx : ('constr, 'types) CRD.pt -> Names.Name.t Context.binder_annot
 
 (* --- Questions about declarations --- *)
 
diff --git a/src/coq/logicutils/hofs/substitution.ml b/src/coq/logicutils/hofs/substitution.ml
index f4f0e2e..702f7e3 100644
--- a/src/coq/logicutils/hofs/substitution.ml
+++ b/src/coq/logicutils/hofs/substitution.ml
@@ -117,7 +117,7 @@ let all_typ_substs_combs : (types * types) comb_substitution =
 
  (* --- Substituting global references --- *)
 
-type global_substitution = global_reference Globnames.Refmap.t
+type global_substitution = Globnames.global_reference GlobRef.Map.t
 
 (* Substitute global references throughout a term *)
 let rec subst_globals subst (term : constr) =
@@ -126,7 +126,7 @@ let rec subst_globals subst (term : constr) =
     (fun _ t ->
       try
         pglobal_of_constr t |>
-        map_puniverses (flip Globnames.Refmap.find subst) |>
+        map_puniverses (flip GlobRef.Map.find subst) |>
         constr_of_pglobal
       with _ ->
         match kind t with
diff --git a/src/coq/logicutils/hofs/substitution.mli b/src/coq/logicutils/hofs/substitution.mli
index 205bcf4..f489d26 100644
--- a/src/coq/logicutils/hofs/substitution.mli
+++ b/src/coq/logicutils/hofs/substitution.mli
@@ -3,7 +3,6 @@
 open Environ
 open Constr
 open Evd
-open Names
 
 (* TODO clean up so retrieval is easier *)
 
@@ -76,7 +75,7 @@ val all_typ_substs_combs : (types * types) comb_substitution
 
 (* --- Substituting global references (TODO unify w/ above after cleaning types) --- *)
 
-type global_substitution = global_reference Globnames.Refmap.t
+type global_substitution = Globnames.global_reference Names.GlobRef.Map.t
 
 (* Substitute global references throughout a term *)
 val subst_globals : global_substitution -> constr -> constr

From 343c23f20d882dc705e20292c6709e97a863633d Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 9 Aug 2022 23:37:14 -0400
Subject: [PATCH 18/42] Exclude more warnings from turning into errors

---
 Makefile.local | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.local b/Makefile.local
index ec5478e..6848028 100644
--- a/Makefile.local
+++ b/Makefile.local
@@ -1 +1 @@
-OCAMLWARN=-warn-error +a-3-8-40
+OCAMLWARN=-warn-error +a-3-8-40-32

From 3eeea211b101c21ceff2b1be7ebd7ed10a135726 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 9 Aug 2022 23:37:42 -0400
Subject: [PATCH 19/42] Port more logicutils

---
 src/coq/logicutils/contexts/envutils.ml   | 12 ++---
 src/coq/logicutils/hofs/filters.ml        |  1 -
 src/coq/logicutils/hofs/hofs.ml           | 60 ++++++++++++++---------
 src/coq/logicutils/hofs/zooming.ml        |  9 ++--
 src/coq/logicutils/inductive/indexing.ml  |  1 -
 src/coq/logicutils/inductive/indutils.ml  | 41 ++++++++++------
 src/coq/logicutils/inductive/indutils.mli |  6 +--
 7 files changed, 73 insertions(+), 57 deletions(-)

diff --git a/src/coq/logicutils/contexts/envutils.ml b/src/coq/logicutils/contexts/envutils.ml
index 3b4ebb5..22593b7 100644
--- a/src/coq/logicutils/contexts/envutils.ml
+++ b/src/coq/logicutils/contexts/envutils.ml
@@ -6,8 +6,6 @@ open Utilities
 open Environ
 open Constr
 open Declarations
-open Decl_kinds
-open Constrextern
 open Contextutils
 open Evd
 open Names
@@ -33,15 +31,15 @@ let lookup_all_rels (env : env) : rel_declaration list =
 (* Return a name-type pair from the given rel_declaration. *)
 let rel_name_type rel : Name.t * types =
   match rel with
-  | CRD.LocalAssum (n, t) -> (n, t)
-  | CRD.LocalDef (n, _, t) -> (n, t)
+  | CRD.LocalAssum (n, t) -> (n.binder_name, t)
+  | CRD.LocalDef (n, _, t) -> (n.binder_name, t)
 
 
 (* Push a local binding to an environment *)
-let push_local (n, t) = push_rel CRD.(LocalAssum (n, t))
+let push_local (n, t) = push_rel CRD.(LocalAssum (get_rel_ctx_name n, t))
 
 (* Push a let-in definition to an environment *)
-let push_let_in (n, e, t) = push_rel CRD.(LocalDef(n, e, t))
+let push_let_in (n, e, t) = push_rel CRD.(LocalDef(get_rel_ctx_name n, e, t))
 
 (* Lookup n rels and remove then *)
 let lookup_pop (n : int) (env : env) =
@@ -53,7 +51,7 @@ let force_constant_body const_body =
   | Def const_def ->
     Mod_subst.force_constr const_def
   | OpaqueDef opaq ->
-    Opaqueproof.force_proof (Global.opaque_tables ()) opaq
+    fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) opaq)
   | _ ->
     CErrors.user_err ~hdr:"force_constant_body"
       (Pp.str "An axiom has no defining term")
diff --git a/src/coq/logicutils/hofs/filters.ml b/src/coq/logicutils/hofs/filters.ml
index 585bae3..96d872b 100644
--- a/src/coq/logicutils/hofs/filters.ml
+++ b/src/coq/logicutils/hofs/filters.ml
@@ -4,7 +4,6 @@ open Constr
 open Environ
 open Debruijn
 open Evd
-open Utilities
 open Checking
 open Inference
 open Stateutils
diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml
index 29bd75a..112ef05 100644
--- a/src/coq/logicutils/hofs/hofs.ml
+++ b/src/coq/logicutils/hofs/hofs.ml
@@ -5,7 +5,6 @@ open Constr
 open Contextutils
 open Envutils
 open Utilities
-open Names
 open Evd
 open Stateutils
 
@@ -147,6 +146,7 @@ let map_rec_env_fix_cartesian (map_rec : ('a, 'b) list_transformer_with_env) d e
  * TODO explain
  *)
 let map_term_env_rec map_rec f d env sigma a trm =
+  let open Context in
   match kind trm with
   | Cast (c, k, t) ->
      let sigma, c' = map_rec env sigma a c in
@@ -154,16 +154,16 @@ let map_term_env_rec map_rec f d env sigma a trm =
      sigma, mkCast (c', k, t')
   | Prod (n, t, b) ->
      let sigma, t' = map_rec env sigma a t in
-     let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, mkProd (n, t', b')
   | Lambda (n, t, b) ->
      let sigma, t' = map_rec env sigma a t in
-     let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, mkLambda (n, t', b')
   | LetIn (n, trm, typ, e) ->
      let sigma, trm' = map_rec env sigma a trm in
      let sigma, typ' = map_rec env sigma a typ in
-     let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+     let sigma, e' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
      sigma, mkLetIn (n, trm', typ', e')
   | App (fu, args) ->
      let sigma, fu' = map_rec env sigma a fu in
@@ -175,12 +175,15 @@ let map_term_env_rec map_rec f d env sigma a trm =
      let sigma, bs' = map_rec_args map_rec env sigma a bs in
      sigma, mkCase (ci, ct', m', bs')
   | Fix ((is, i), (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, ts' = map_rec_args map_rec env sigma a ts in
-     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, ds' = map_rec_args 
+       (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, mkFix ((is, i), (ns, ts', ds'))
   | CoFix (i, (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, ts' = map_rec_args map_rec env sigma a ts in
-     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, mkCoFix (i, (ns, ts', ds'))
   | Proj (p, c) ->
      let sigma, c' = map_rec env sigma a c in
@@ -216,6 +219,7 @@ let map_term f d a trm =
  * TODO explain
  *)
 let map_subterms_env_rec map_rec f d env sigma a trm =
+  let open Context in
   match kind trm with
   | Cast (c, k, t) ->
      let sigma, cs' = map_rec env sigma a c in
@@ -223,16 +227,16 @@ let map_subterms_env_rec map_rec f d env sigma a trm =
      sigma, combine_cartesian (fun c' t' -> mkCast (c', k, t')) cs' ts'
   | Prod (n, t, b) ->
      let sigma, ts' = map_rec env sigma a t in
-     let sigma, bs' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, bs' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, combine_cartesian (fun t' b' -> mkProd (n, t', b')) ts' bs'
   | Lambda (n, t, b) ->
      let sigma, ts' = map_rec env sigma a t in
-     let sigma, bs' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, bs' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, combine_cartesian (fun t' b' -> mkLambda (n, t', b')) ts' bs'
   | LetIn (n, trm, typ, e) ->
      let sigma, trms' = map_rec env sigma a trm in
      let sigma, typs' = map_rec env sigma a typ in
-     let sigma, es' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+     let sigma, es' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
      sigma, combine_cartesian (fun trm' (typ', e') -> mkLetIn (n, trm', typ', e')) trms' (cartesian typs' es')
   | App (fu, args) ->
      let sigma, fus' = map_rec env sigma a fu in
@@ -244,12 +248,14 @@ let map_subterms_env_rec map_rec f d env sigma a trm =
      let sigma, bss' = map_rec_args_cartesian map_rec env sigma a bs in
      sigma, combine_cartesian (fun ct' (m', bs') -> mkCase (ci, ct', m', bs')) cts' (cartesian ms' bss')
   | Fix ((is, i), (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, tss' = map_rec_args_cartesian map_rec env sigma a ts in
-     let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, combine_cartesian (fun ts' ds' -> mkFix ((is, i), (ns, ts', ds'))) tss' dss'
   | CoFix (i, (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, tss' = map_rec_args_cartesian map_rec env sigma a ts in
-     let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, combine_cartesian (fun ts' ds' -> mkCoFix (i, (ns, ts', ds'))) tss' dss'
   | Proj (p, c) ->
      let sigma, cs' = map_rec env sigma a c in
@@ -309,6 +315,7 @@ let rec map_term_env_if p f d env sigma a trm =
  * TODO explain
  *)
 let map_term_env_rec_shallow map_rec f d env sigma a trm =
+  let open Context in
   match kind trm with
   | Cast (c, k, t) ->
      let sigma, c' = map_rec env sigma a c in
@@ -316,16 +323,16 @@ let map_term_env_rec_shallow map_rec f d env sigma a trm =
      sigma, mkCast (c', k, t')
   | Prod (n, t, b) ->
      let sigma, t' = map_rec env sigma a t in
-     let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, mkProd (n, t', b')
   | Lambda (n, t, b) ->
      let sigma, t' = map_rec env sigma a t in
-     let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+     let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
      sigma, mkLambda (n, t', b')
   | LetIn (n, trm, typ, e) ->
      let sigma, trm' = map_rec env sigma a trm in
      let sigma, typ' = map_rec env sigma a typ in
-     let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+     let sigma, e' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
      sigma, mkLetIn (n, trm', typ', e')
   | App (fu, args) ->
      let sigma, fu' = map_rec env sigma a fu in
@@ -340,12 +347,14 @@ let map_term_env_rec_shallow map_rec f d env sigma a trm =
      let sigma, bs' = map_rec_args map_rec env sigma a bs in
      sigma, mkCase (ci, ct', m', bs')
   | Fix ((is, i), (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, ts' = map_rec_args map_rec env sigma a ts in
-     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, mkFix ((is, i), (ns, ts', ds'))
   | CoFix (i, (ns, ts, ds)) ->
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
      let sigma, ts' = map_rec_args map_rec env sigma a ts in
-     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *)
+     let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns_binder_name ts trm) env sigma a ds in (* TODO refactor *)
      sigma, mkCoFix (i, (ns, ts', ds'))
   | Proj (p, c) ->
      let sigma, c' = map_rec env sigma a c in
@@ -483,6 +492,7 @@ let rec map_subterms_env_if_combs p f d env sigma a trm =
  * Like map_term_env_if, but make a list of subterm results
  *)
 let rec map_term_env_if_list p f d env sigma a trm =
+  let open Context in
   let map_rec = map_term_env_if_list p f d in
   let sigma_t, p_holds = p env sigma a trm in
   let new_subterms = if p_holds
@@ -495,16 +505,16 @@ let rec map_term_env_if_list p f d env sigma a trm =
        List.append c' t'
     | Prod (n, t, b) ->
        let t' = map_rec env sigma a t in
-       let b' = map_rec (push_local (n, t) env) sigma (d a) b in
+       let b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
        List.append t' b'
     | Lambda (n, t, b) ->
        let t' = map_rec env sigma a t in
-       let b' = map_rec (push_local (n, t) env) sigma (d a) b in
+       let b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
        List.append t' b'
     | LetIn (n, trm, typ, e) ->
        let trm' = map_rec env sigma a trm in
        let typ' = map_rec env sigma a typ in
-       let e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+       let e' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
        List.append trm' (List.append typ' e')
     | App (fu, args) ->
        let fu' = map_rec env sigma a fu in
@@ -516,12 +526,14 @@ let rec map_term_env_if_list p f d env sigma a trm =
        let bs' = Array.map (map_rec env sigma a) bs in
        List.append ct' (List.append m' (List.flatten (Array.to_list bs')))
     | Fix ((is, i), (ns, ts, ds)) ->
+       let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
        let ts' = Array.map (map_rec env sigma a) ts in
-       let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns ts) ds in
+       let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns_binder_name ts) ds in
        List.append (List.flatten (Array.to_list ts')) (List.flatten (Array.to_list ds'))
     | CoFix (i, (ns, ts, ds)) ->
+       let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
        let ts' = Array.map (map_rec env sigma a) ts in
-       let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns ts) ds in
+       let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns_binder_name ts) ds in
        List.append (List.flatten (Array.to_list ts')) (List.flatten (Array.to_list ds'))
     | Proj (pr, c) ->
        map_rec env sigma a c
@@ -580,16 +592,16 @@ let rec exists_subterm_env p d env sigma (a : 'a) (trm : types) : evar_map * boo
          sigma, c' || t'
       | Prod (n, t, b) ->
          let sigma, t' = map_rec env sigma a t in
-         let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+         let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
          sigma, t' || b'
       | Lambda (n, t, b) ->
          let sigma, t' = map_rec env sigma a t in
-         let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in
+         let sigma, b' = map_rec (push_local (n.binder_name, t) env) sigma (d a) b in
          sigma, t' || b'
       | LetIn (n, trm, typ, e) ->
          let sigma, trm' = map_rec env sigma a trm in
          let sigma, typ' = map_rec env sigma a typ in
-         let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in
+         let sigma, e' = map_rec (push_let_in (n.binder_name, e, typ) env) sigma (d a) e in
          sigma, trm' || typ' || e'
       | App (fu, args) ->
          let sigma, fu' = map_rec env sigma a fu in
diff --git a/src/coq/logicutils/hofs/zooming.ml b/src/coq/logicutils/hofs/zooming.ml
index 722b554..ce68ff6 100644
--- a/src/coq/logicutils/hofs/zooming.ml
+++ b/src/coq/logicutils/hofs/zooming.ml
@@ -10,7 +10,6 @@ open Envutils
 open Contextutils
 open Debruijn
 open Sigmautils
-open Evd
 open Names
 
 (* --- Zooming --- *)
@@ -22,7 +21,7 @@ let rec zoom_n_prod env npm typ : env * types =
   else
     match kind typ with
     | Prod (n1, t1, b1) ->
-       zoom_n_prod (push_local (n1, t1) env) (npm - 1) b1
+       zoom_n_prod (push_local (n1.binder_name, t1) env) (npm - 1) b1
     | _ ->
        failwith "more parameters expected"
 
@@ -35,7 +34,7 @@ let zoom_n_lambda env npm trm : env * types =
 let rec zoom_lambda_term (env : env) (trm : types) : env * types =
   match kind trm with
   | Lambda (n, t, b) ->
-     zoom_lambda_term (push_local (n, t) env) b
+     zoom_lambda_term (push_local (n.binder_name, t) env) b
   | _ ->
      (env, trm)
 
@@ -43,7 +42,7 @@ let rec zoom_lambda_term (env : env) (trm : types) : env * types =
 let rec zoom_product_type (env : env) (typ : types) : env * types =
   match kind typ with
   | Prod (n, t, b) ->
-     zoom_product_type (push_local (n, t) env) b
+     zoom_product_type (push_local (n.binder_name, t) env) b
   | _ ->
      (env, typ)
 
@@ -56,7 +55,7 @@ let zoom_lambda_names env except trm : env * types * Id.t list =
     | limit ->
      match kind trm with
      | Lambda (n, t, b) ->
-        let name = fresh_name env n in
+        let name = fresh_name env n.binder_name in
         let env' = push_local (Name name, t) env in
         let env, trm, names =
           aux env' (limit - 1) b in
diff --git a/src/coq/logicutils/inductive/indexing.ml b/src/coq/logicutils/inductive/indexing.ml
index b01d640..9746731 100644
--- a/src/coq/logicutils/inductive/indexing.ml
+++ b/src/coq/logicutils/inductive/indexing.ml
@@ -10,7 +10,6 @@ open Hofimpls
 open Reducers
 open Sigmautils
 open Apputils
-open Evd
 
 (* --- Generic functions --- *)
 
diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml
index c8c1b5b..e22310b 100644
--- a/src/coq/logicutils/inductive/indutils.ml
+++ b/src/coq/logicutils/inductive/indutils.ml
@@ -31,7 +31,7 @@ let check_inductive_supported mutind_body : unit =
 let inductive_of_elim (env : env) (pc : pconstant) : MutInd.t option =
   let (c, u) = pc in
   let kn = Constant.canonical c in
-  let (modpath, dirpath, label) = KerName.repr kn in
+  let (modpath, label) = KerName.repr kn in
   let rec try_find_ind is_rev =
     try
       let label_string = Label.to_string label in
@@ -42,7 +42,7 @@ let inductive_of_elim (env : env) (pc : pconstant) : MutInd.t option =
       if (suffix = "_ind" || suffix = "_rect" || suffix = "_rec" || suffix = "_ind_r") then
         let ind_label_string = String.sub label_string 0 split_index in
         let ind_label = Label.of_id (Id.of_string_soft ind_label_string) in
-        let ind_name = MutInd.make1 (KerName.make modpath dirpath ind_label) in
+        let ind_name = MutInd.make1 (KerName.make modpath ind_label) in
         let _ = lookup_mind ind_name env in
         Some ind_name
       else
@@ -78,7 +78,10 @@ let is_elim (env : env) (trm : types) =
 
 (* Lookup the eliminator over the type sort *)
 let type_eliminator (env : env) (ind : inductive) =
-  Universes.constr_of_global (Indrec.lookup_eliminator ind InType)
+  UnivGen.constr_of_monomorphic_global (Indrec.lookup_eliminator env ind InType)
+  (* TODO: Does this need to support polymorphic (and not just monomorphic)?
+     E.g.: Evd.fresh_global env (Evd.from_env env) (Indrec.lookup_eliminator env ind InType) 
+   *)
 
 (* Applications of eliminators *)
 type elim_app =
@@ -125,9 +128,9 @@ let rec num_ihs env sigma rec_typ typ =
      let t_red = reduce_stateless reduce_term env sigma t in
      if is_or_applies rec_typ t_red then
        let (n_b_t, b_t, b_b) = destProd b in
-       1 + num_ihs (push_local (n, t) (push_local (n_b_t, b_t) env)) sigma rec_typ b_b
+       1 + num_ihs (push_local (n.binder_name, t) (push_local (n_b_t.binder_name, b_t) env)) sigma rec_typ b_b
      else
-       num_ihs (push_local (n, t) env) sigma rec_typ b
+       num_ihs (push_local (n.binder_name, t) env) sigma rec_typ b
   | _ ->
      0
 
@@ -147,6 +150,7 @@ let arity_of_ind_body ind_body =
     recompose_prod_assum ind_body.mind_arity_ctxt sort
 
 (* Create an Entries.local_entry from a Rel.Declaration.t *)
+(*
 let make_ind_local_entry decl =
   let entry =
     match decl with
@@ -156,35 +160,39 @@ let make_ind_local_entry decl =
   match CRD.get_name decl with
   | Name.Name id -> (id, entry)
   | Name.Anonymous -> failwith "Parameters to an inductive type may not be anonymous"
+*)
 
 (* Instantiate an abstract universe context *)
 let inst_abs_univ_ctx abs_univ_ctx =
   (* Note that we're creating *globally* fresh universe levels. *)
-  Universes.fresh_instance_from_context abs_univ_ctx |> Univ.UContext.make
+   UnivGen.fresh_instance abs_univ_ctx
 
 (* Instantiate an abstract_inductive_universes into an Entries.inductive_universes with Univ.UContext.t (TODO do we do something with evar_map here?) *)
 let make_ind_univs_entry = function
-  | Monomorphic_ind univ_ctx_set ->
+  | Monomorphic univ_ctx_set ->
     let univ_ctx = Univ.UContext.empty in
-    (Entries.Monomorphic_ind_entry univ_ctx_set, univ_ctx)
-  | Polymorphic_ind abs_univ_ctx ->
-    let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in
-    (Entries.Polymorphic_ind_entry univ_ctx, univ_ctx)
+    (Entries.Monomorphic_entry univ_ctx_set, univ_ctx)
+  | Polymorphic abs_univ_ctx ->
+    let univ_ctx_repr = (Univ.AUContext.repr abs_univ_ctx) in
+    (Entries.Polymorphic_entry 
+      (Univ.AUContext.names abs_univ_ctx, univ_ctx_repr), univ_ctx_repr)
+(*
   | Cumulative_ind abs_univ_cumul ->
     let abs_univ_ctx = Univ.ACumulativityInfo.univ_context abs_univ_cumul in
     let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in
     let univ_var = Univ.ACumulativityInfo.variance abs_univ_cumul in
     let univ_cumul = Univ.CumulativityInfo.make (univ_ctx, univ_var) in
     (Entries.Cumulative_ind_entry univ_cumul, univ_ctx)
+*)
 
 let open_inductive ?(global=false) env (mind_body, ind_body) =
   let univs, univ_ctx = make_ind_univs_entry mind_body.mind_universes in
   let subst_univs = Vars.subst_instance_constr (Univ.UContext.instance univ_ctx) in
   let env = Environ.push_context univ_ctx env in
   if global then
-    Global.push_context false univ_ctx;
+    Global.push_context_set false (Univ.ContextSet.of_context univ_ctx);
   let arity = arity_of_ind_body ind_body in
-  let arity_ctx = [CRD.LocalAssum (Name.Anonymous, arity)] in
+  let arity_ctx = [CRD.LocalAssum (get_rel_ctx_name Name.Anonymous, arity)] in
   let ctors_typ = Array.map (recompose_prod_assum arity_ctx) ind_body.mind_user_lc in
   env, univs, subst_univs arity, Array.map_to_list subst_univs ctors_typ
 
@@ -202,13 +210,14 @@ let declare_inductive typename consnames template univs nparam arity constypes =
   let mind_entry =
     { mind_entry_record = None;
       mind_entry_finite = Declarations.Finite;
-      mind_entry_params = List.map make_ind_local_entry params;
+      mind_entry_params = params;
       mind_entry_inds = [ind_entry];
       mind_entry_universes = univs;
+      mind_entry_variance = None;
       mind_entry_private = None }
   in
-  let ((_, ker_name), _) = Declare.declare_mind mind_entry in
-  let mind = MutInd.make1 ker_name in
+  let mind = DeclareInd.declare_mutual_inductive_with_eliminations mind_entry UnivNames.empty_binders [] in
+  (* let mind = MutInd.make1 ker_name in *)
   let ind = (mind, 0) in
   Indschemes.declare_default_schemes mind;
   ind
diff --git a/src/coq/logicutils/inductive/indutils.mli b/src/coq/logicutils/inductive/indutils.mli
index 502e99b..9c484b8 100644
--- a/src/coq/logicutils/inductive/indutils.mli
+++ b/src/coq/logicutils/inductive/indutils.mli
@@ -69,9 +69,9 @@ val arity_of_ind_body : one_inductive_body -> types
  * universe levels, and return the universe-synchronized environment. If global
  * is true, the global environment is also synchronized with the new universe
  * levels and constraints. A descriptor for the inductive type's universe
- * properties is also returned.
+ * properties is also returned. Mutual inductive types are not supported.
  *)
-val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entries.inductive_universes * types * types list
+val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entries.universes_entry * types * types list
 
 (*
  * Declare a new inductive type in the global environment. Note that the arity
@@ -79,5 +79,5 @@ val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entri
  * a recursive reference and then all parameters (i.e.,
  * forall (I : arity) (P : params), ...).
  *)
-val declare_inductive : Id.t -> Id.t list -> bool -> Entries.inductive_universes -> int -> types -> types list -> inductive
+val declare_inductive : Id.t -> Id.t list -> bool -> Entries.universes_entry -> int -> types -> types list -> inductive
 

From a7c7ae1328fa8cd467c1c36f0515a57557de64ad Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Sun, 14 Aug 2022 17:17:10 -0400
Subject: [PATCH 20/42] Port modutils

---
 src/coq/logicutils/contexts/modutils.ml  | 14 ++++++++------
 src/coq/logicutils/contexts/modutils.mli | 12 ++++++++----
 2 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/coq/logicutils/contexts/modutils.ml b/src/coq/logicutils/contexts/modutils.ml
index 709ab84..e204268 100644
--- a/src/coq/logicutils/contexts/modutils.ml
+++ b/src/coq/logicutils/contexts/modutils.ml
@@ -25,9 +25,10 @@ let decompose_module_signature mod_sign =
  * The optional argument specifies functor parameters.
  *)
 let declare_module_structure ?(params=[]) ident declare_elements =
-  let mod_sign = Vernacexpr.Check [] in
+  let mod_sign = Declaremods.Check []in
   let mod_path =
-    Declaremods.start_module Modintern.interp_module_ast None ident params mod_sign
+    (* Declaremods.start_module None ident params Modintern.interp_module_ast mod_sign *)
+    Declaremods.start_module None ident params mod_sign
   in
   Dumpglob.dump_moddef mod_path "mod";
   declare_elements mod_path;
@@ -55,7 +56,7 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body =
     match mod_elem with
     | SFBconst const_body ->
       let const = Constant.make2 mod_path label in
-      if Refset.mem (ConstRef const) globset then
+      if Names.GlobRef.Set.mem (ConstRef const) globset then
         (globset, acc)
       else
         (globset, fold_const acc const const_body)
@@ -63,9 +64,10 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body =
       check_inductive_supported mind_body;
       let ind_body = mind_body.mind_packets.(0) in
       let ind = (MutInd.make2 mod_path label, 0) in
+      let env = Global.env () in (* might need to pass something other than an empty env *)
       let globset' =
-        List.map (Indrec.lookup_eliminator ind) ind_body.mind_kelim |>
-        List.fold_left (fun gset gref -> Refset.add gref gset) globset
+        List.map (Indrec.lookup_eliminator env ind) [ind_body.mind_kelim] |>
+        List.fold_left (fun gset gref -> Names.GlobRef.Set.add gref gset) globset
       in
       (globset', fold_ind acc ind (mind_body, ind_body))
     | SFBmodule mod_body ->
@@ -77,7 +79,7 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body =
         Pp.(str "Skipping nested module signature " ++ Label.print label);
       (globset, acc)
   in
-  fold_module_structure_by_elem (Refset.empty, init) fold_mod_elem mod_body |> snd
+  fold_module_structure_by_elem (Names.GlobRef.Set.empty, init) fold_mod_elem mod_body |> snd
 
 (*
  * Same as `fold_module_structure_by_decl` except a single step function
diff --git a/src/coq/logicutils/contexts/modutils.mli b/src/coq/logicutils/contexts/modutils.mli
index b1becf4..5e561d5 100644
--- a/src/coq/logicutils/contexts/modutils.mli
+++ b/src/coq/logicutils/contexts/modutils.mli
@@ -15,7 +15,7 @@ val decompose_module_signature : module_signature -> (Names.MBId.t * module_type
  *
  * The optional argument specifies functor parameters.
  *)
-val declare_module_structure : ?params:(Constrexpr.module_ast Declaremods.module_params) -> Id.t -> (ModPath.t -> unit) -> ModPath.t
+val declare_module_structure : ?params:(Declaremods.module_params) -> Id.t -> (ModPath.t -> unit) -> ModPath.t
 
 (*
  * Fold over the constant/inductive definitions within a module structure,
@@ -24,15 +24,19 @@ val declare_module_structure : ?params:(Constrexpr.module_ast Declaremods.module
  *
  * Elimination schemes (e.g., `Ind_rect`) are filtered out from the definitions.
  *)
-val fold_module_structure_by_decl : 'a -> ('a -> Constant.t -> constant_body -> 'a) -> ('a -> inductive -> Inductive.mind_specif -> 'a) -> module_body -> 'a
+(* val fold_module_structure_by_decl : 'a -> ('a -> Constant.t -> 'opaque constant_body -> 'a) -> ('a -> inductive -> Inductive.mind_specif -> 'a) -> module_body -> 'a 
+val fold_module_structure_by_decl : 'a -> ('a -> Names.Constant.t -> 'opaque Declarations.constant_body -> 'a) -> ('a -> Names.inductive -> Inductive.mind_specif -> 'a) -> Declarations.module_body -> 'a *)
+val fold_module_structure_by_decl : 'a -> ('a -> Names.Constant.t -> Opaqueproof.opaque Declarations.constant_body -> 'a) -> ('a -> Names.MutInd.t * int -> Declarations.mutual_inductive_body * Declarations.one_inductive_body -> 'a) -> 'b Declarations.generic_module_body -> 'a
 
 (*
  * Same as `fold_module_structure_by_decl` except a single step function
  * accepting a global reference.
  *)
-val fold_module_structure_by_glob : 'a -> ('a -> global_reference -> 'a) -> module_body -> 'a
+(* val fold_module_structure_by_glob : 'a -> ('a -> evaluable_global_reference -> 'a) -> module_body -> 'a *)
+val fold_module_structure_by_glob : 'a -> ('a -> Names.evaluable_global_reference -> 'a) -> Declarations.module_body -> 'a
 
 (*
  * Same as `fold_module_structure_by_glob` except an implicit unit accumulator.
  *)
-val iter_module_structure_by_glob : (global_reference -> unit) -> module_body -> unit
+(* val iter_module_structure_by_glob : (evaluable_global_reference -> unit) -> module_body -> unit *)
+val fold_module_structure_by_glob : 'a -> ('a -> Globnames.global_reference -> 'a) -> 'b Declarations.generic_module_body -> 'a

From cd437545af79af778d8198e94b375e021196bc43 Mon Sep 17 00:00:00 2001
From: Max Fan <root@max.fan>
Date: Tue, 16 Aug 2022 10:05:09 -0400
Subject: [PATCH 21/42] Partial port of transform.ml and transform.mli

---
 src/coq/logicutils/transformation/transform.ml  | 7 ++++---
 src/coq/logicutils/transformation/transform.mli | 4 ++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml
index 1a786ad..a4d7103 100644
--- a/src/coq/logicutils/transformation/transform.ml
+++ b/src/coq/logicutils/transformation/transform.ml
@@ -15,6 +15,7 @@ open Indutils
 open Substitution
 open Stateutils
 open Recordops
+open Record
 
 (* Type-sensitive transformation of terms *)
 type constr_transformer = env -> evar_map -> constr -> evar_map * constr
@@ -28,7 +29,7 @@ let force_constant_body const_body =
   | Def const_def ->
     Mod_subst.force_constr const_def
   | OpaqueDef opaq ->
-    Opaqueproof.force_proof (Global.opaque_tables ()) opaq
+    fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) opaq)
   | _ ->
     CErrors.user_err ~hdr:"force_constant_body"
       (Pp.str "An axiom has no defining term")
@@ -43,9 +44,9 @@ let force_constant_body const_body =
 let transform_constant ident tr_constr const_body =
   let env =
     match const_body.const_universes with
-    | Monomorphic_const univs ->
+    | Monomorphic  univs ->
       Global.env () |> Environ.push_context_set univs
-    | Polymorphic_const univs ->
+    | Polymorphic univs ->
       CErrors.user_err ~hdr:"transform_constant"
         Pp.(str "Universe polymorphism is not supported")
   in
diff --git a/src/coq/logicutils/transformation/transform.mli b/src/coq/logicutils/transformation/transform.mli
index 68c42f1..81c4aaf 100644
--- a/src/coq/logicutils/transformation/transform.mli
+++ b/src/coq/logicutils/transformation/transform.mli
@@ -20,7 +20,7 @@ type constr_transformer = env -> evar_map -> constr -> evar_map * constr
  * NOTE: Global side effects.
  *)
 val transform_constant :
-  Id.t -> constr_transformer -> constant_body -> evar_map * Constant.t
+  Id.t -> constr_transformer -> 'opaque constant_body -> evar_map * Constant.t
 
 (*
  * Declare a new inductive family under the given name with the transformed type
@@ -45,4 +45,4 @@ val transform_inductive :
  * NOTE: Global side effects.
  *)
 val transform_module_structure :
-  ?init:(unit -> global_substitution) -> ?opaques:(Globnames.Refset.t) -> Id.t -> constr_transformer -> module_body -> ModPath.t
+  ?init:(unit -> global_substitution) -> ?opaques:(Names.GlobRef.Set.t) -> Id.t -> constr_transformer -> module_body -> ModPath.t

From 6d2b00973822302712c403bcf47c02e166895fe1 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Fri, 19 Aug 2022 18:35:41 -0400
Subject: [PATCH 22/42] Finish porting transform

---
 .../logicutils/transformation/transform.ml    | 30 +++++--------------
 .../logicutils/transformation/transform.mli   |  2 +-
 2 files changed, 8 insertions(+), 24 deletions(-)

diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml
index a4d7103..83b70dc 100644
--- a/src/coq/logicutils/transformation/transform.ml
+++ b/src/coq/logicutils/transformation/transform.ml
@@ -90,14 +90,8 @@ let try_register_record mod_path (ind, ind') =
   try
     let r = lookup_structure ind in
     Feedback.msg_info (Pp.str "Transformed a record");
-    let pks = r.s_PROJKIND in
-    let ps =
-      List.map
-        (Option.map (fun p -> Constant.make2 mod_path (Constant.label p)))
-        r.s_PROJ
-    in
     (try
-       declare_structure (ind', (ind', 1), pks, ps)
+       declare_structure_entry (r.s_CONST, r.s_PROJKIND, r.s_PROJ)
      with _ ->
        Feedback.msg_warning
          (Pp.str "Failed to register projections for transformed record"))
@@ -118,7 +112,7 @@ let try_register_record mod_path (ind, ind') =
  *
  * TODO sigma handling, not sure how to do it here/if we need it
  *)
-let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Globnames.Refset.empty) ident tr_constr mod_body =
+let transform_module_structure ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef.Set.empty) ident tr_constr mod_body =
   let open Modutils in
   let mod_path = mod_body.mod_mp in
   let mod_arity, mod_elems = decompose_module_signature mod_body.mod_type in
@@ -128,7 +122,7 @@ let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Gl
         match b with
         | SFBconst const_body ->
            let const = Constant.make2 mod_path l in
-           not (Globnames.Refset.mem (ConstRef const) opaques)
+           not (GlobRef.Set.mem (ConstRef const) opaques)
         | _ ->
            true)
       mod_elems
@@ -142,24 +136,14 @@ let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Gl
     match body with
     | SFBconst const_body ->
       let const = Constant.make2 mod_path label in
-      if Globnames.Refmap.mem (ConstRef const) subst then
+      if GlobRef.Map.mem (ConstRef const) subst then
         subst (* Do not transform schematic definitions. *)
       else
         let sigma, const' = transform_constant ident tr_constr const_body in
-        Globnames.Refmap.add (ConstRef const) (ConstRef const') subst
+        GlobRef.Map.add (ConstRef const) (ConstRef const') subst
     | SFBmind mind_body ->
-      check_inductive_supported mind_body;
-      let ind = (MutInd.make2 mod_path label, 0) in
-      let ind_body = mind_body.mind_packets.(0) in
-      let sigma, ind' = transform_inductive ident tr_constr (mind_body, ind_body) in
-      try_register_record mod_path' (ind, ind');
-      let ncons = Array.length ind_body.mind_consnames in
-      let list_cons ind = List.init ncons (fun i -> ConstructRef (ind, i + 1)) in
-      let sorts = ind_body.mind_kelim in
-      let list_elim ind = List.map (Indrec.lookup_eliminator ind) sorts in
-      Globnames.Refmap.add (IndRef ind) (IndRef ind') subst |>
-      List.fold_right2 Globnames.Refmap.add (list_cons ind) (list_cons ind') |>
-      List.fold_right2 Globnames.Refmap.add (list_elim ind) (list_elim ind')
+      Feedback.msg_warning (Pp.str "Mutually inductive types are not supported");
+      subst
     | SFBmodule mod_body ->
       Feedback.msg_warning (Pp.str "Skipping nested module structure");
       subst
diff --git a/src/coq/logicutils/transformation/transform.mli b/src/coq/logicutils/transformation/transform.mli
index 81c4aaf..79b32ab 100644
--- a/src/coq/logicutils/transformation/transform.mli
+++ b/src/coq/logicutils/transformation/transform.mli
@@ -20,7 +20,7 @@ type constr_transformer = env -> evar_map -> constr -> evar_map * constr
  * NOTE: Global side effects.
  *)
 val transform_constant :
-  Id.t -> constr_transformer -> 'opaque constant_body -> evar_map * Constant.t
+  Id.t -> constr_transformer -> Opaqueproof.opaque constant_body -> evar_map * Constant.t
 
 (*
  * Declare a new inductive family under the given name with the transformed type

From fad8b1e57b2cd2c6b1b56f1b8180276047ed12c1 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Fri, 19 Aug 2022 18:37:06 -0400
Subject: [PATCH 23/42] Port devutils/printing

---
 src/coq/devutils/printing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq/devutils/printing.mli b/src/coq/devutils/printing.mli
index d4dc67d..e90a439 100644
--- a/src/coq/devutils/printing.mli
+++ b/src/coq/devutils/printing.mli
@@ -8,7 +8,7 @@ open Evd
 (* --- Coq terms --- *)
 
 (* Pretty-print a `global_reference` with fancy `constr` coloring. *)
-val pr_global_as_constr : global_reference -> Pp.t
+val pr_global_as_constr : Globnames.global_reference -> Pp.t
 
 (* Gets a name as a string *)
 val name_as_string : Name.t -> string

From c425423d6da180ac2c08ddccccea13d604fbe89e Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Fri, 19 Aug 2022 18:39:42 -0400
Subject: [PATCH 24/42] Turn more warnings back to warnings

---
 Makefile.local               |  2 +-
 src/coq/devutils/printing.ml | 24 +++++++++++++-----------
 2 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/Makefile.local b/Makefile.local
index 6848028..e1a43fb 100644
--- a/Makefile.local
+++ b/Makefile.local
@@ -1 +1 @@
-OCAMLWARN=-warn-error +a-3-8-40-32
+OCAMLWARN=-warn-error +a-3-8-40-32-28
diff --git a/src/coq/devutils/printing.ml b/src/coq/devutils/printing.ml
index 51787a2..1c009a5 100644
--- a/src/coq/devutils/printing.ml
+++ b/src/coq/devutils/printing.ml
@@ -24,7 +24,7 @@ module CRD = Context.Rel.Declaration
 let pr_global_as_constr gref =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  pr_constr_env env sigma (Universes.constr_of_global gref)
+  pr_constr_env env sigma (UnivGen.constr_of_monomorphic_global gref)
 
 (* Using pp, prints directly to a string *)
 let print_to_string (pp : formatter -> 'a -> unit) (trm : 'a) : string =
@@ -66,11 +66,12 @@ let sort_as_string s =
 
 (* Prints a term *)
 let rec term_as_string (env : env) (trm : types) =
+  let open Context in
   match kind trm with
   | Rel i ->
      (try
        let (n, _, _) = CRD.to_tuple @@ lookup_rel i env in
-       Printf.sprintf "(%s [Rel %d])" (name_as_string n) i
+       Printf.sprintf "(%s [Rel %d])" (name_as_string n.binder_name) i
      with
        Not_found -> Printf.sprintf "(Unbound_Rel %d)" i)
   | Var v ->
@@ -84,22 +85,22 @@ let rec term_as_string (env : env) (trm : types) =
   | Prod (n, t, b) ->
      Printf.sprintf
        "(Π (%s : %s) . %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env t)
-       (term_as_string (push_local (n, t) env) b)
+       (term_as_string (push_local (n.binder_name, t) env) b)
   | Lambda (n, t, b) ->
      Printf.sprintf
        "(λ (%s : %s) . %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env t)
-       (term_as_string (push_local (n, t) env) b)
+       (term_as_string (push_local (n.binder_name, t) env) b)
   | LetIn (n, trm, typ, e) ->
      Printf.sprintf
        "(let (%s : %s) := %s in %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env typ)
        (term_as_string env trm)
-       (term_as_string (push_let_in (n, trm, typ) env) e)
+       (term_as_string (push_let_in (n.binder_name, trm, typ) env) e)
   | App (f, xs) ->
      Printf.sprintf
        "(%s %s)"
@@ -119,14 +120,15 @@ let rec term_as_string (env : env) (trm : types) =
      let name_id = (ind_bodies.(i_index)).mind_typename in
      Id.to_string name_id
   | Fix ((is, i), (ns, ts, ds)) ->
-     let env_fix = push_rel_context (bindings_for_fix ns ds) env in
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
+     let env_fix = push_rel_context (bindings_for_fix ns_binder_name ds) env in
      String.concat
        " with "
        (map3
           (fun n t d ->
             Printf.sprintf
              "(Fix %s : %s := %s)"
-             (name_as_string n)
+             (name_as_string n.binder_name)
              (term_as_string env t)
              (term_as_string env_fix d))
           (Array.to_list ns)
@@ -180,7 +182,7 @@ let env_as_string (env : env) : string =
          let (n, b, t) = CRD.to_tuple @@ lookup_rel i env in
          Printf.sprintf
            "%s (Rel %d): %s"
-           (name_as_string n)
+           (name_as_string n.binder_name)
            i
            (term_as_string (pop_rel_context i env) t))
        all_relis)

From 53b15cd80ccaba2141fc595bade980c2bd7a0534 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Fri, 19 Aug 2022 19:02:15 -0400
Subject: [PATCH 25/42] Port decompiler

---
 src/coq/decompiler/decompiler.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml
index a7c24bd..98b50fa 100644
--- a/src/coq/decompiler/decompiler.ml
+++ b/src/coq/decompiler/decompiler.ml
@@ -36,11 +36,11 @@ let parse_tac_str (s : string) : unit Proofview.tactic =
 (* Run a coq tactic against a given goal, returning generated subgoals *)
 let run_tac env sigma (tac : unit Proofview.tactic) (goal : constr)
     : Goal.goal list * Evd.evar_map =
-  let p = Proof.start sigma [(env, EConstr.of_constr goal)] in
-  let (p', _) = Proof.run_tactic env tac p in
-  let (subgoals, _, _, _, sigma) = Proof.proof p' in
-  subgoals, sigma
-    
+  let p = Proof.start ~name:(destVar goal) ~poly:true sigma [(env, EConstr.of_constr goal)] in
+  let (p', _, _) = Proof.run_tactic env tac p in
+  let compact_p = Proof.data (Proof.compact p') in
+  (compact_p.goals, compact_p.sigma)
+
 (* Returns true if the given tactic solves the goal. *)
 let solves env sigma (tac : unit Proofview.tactic) (goal : constr) : bool state =
   try
@@ -476,7 +476,7 @@ and apply_in (n, valu, typ, body) (env, sigma, opts) : tactical option =
     
 (* Last resort decompile let-in as a pose.  *)
 and pose (n, valu, t, body) (env, sigma, opts) : tactical option =
-  let n' = fresh_name env n in
+  let n' = fresh_name env n.binder_name in
   let env' = push_let_in (Name n', valu, t) env in
   let decomp_body = first_pass env' sigma opts body in
   (* If the binding is NEVER used, just skip this. *)

From 36c0ba063839d7cb2b37c8e412a28326500dd5da Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Fri, 19 Aug 2022 19:15:22 -0400
Subject: [PATCH 26/42] Fix invalid forward reference issue by rearranging
 imports

---
 src/plib.mlpack | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plib.mlpack b/src/plib.mlpack
index 2d376a0..35ddd3a 100644
--- a/src/plib.mlpack
+++ b/src/plib.mlpack
@@ -18,8 +18,8 @@ Idutils
 Proputils
 
 Stateutils
-Envutils
 Contextutils
+Envutils
 
 Hofs
 Debruijn

From 1e441c419c48938fdbdaf711583564934d04762d Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Fri, 19 Aug 2022 19:30:56 -0400
Subject: [PATCH 27/42] Remove unnecessary plibrary.ml build artifact

---
 .gitignore      | 1 +
 src/plibrary.ml | 2 --
 2 files changed, 1 insertion(+), 2 deletions(-)
 delete mode 100644 src/plibrary.ml

diff --git a/.gitignore b/.gitignore
index bc89608..1d0a03f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -23,3 +23,4 @@ plugin/Makefile
 plugin/.merlin
 *.out
 _opam
+src/plibrary.ml
diff --git a/src/plibrary.ml b/src/plibrary.ml
deleted file mode 100644
index 9993ab4..0000000
--- a/src/plibrary.ml
+++ /dev/null
@@ -1,2 +0,0 @@
-let __coq_plugin_name = "plib"
-let _ = Mltop.add_known_module __coq_plugin_name

From c249fd9bf3418696ca411ce481b0b081dc98d56c Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Fri, 19 Aug 2022 19:33:32 -0400
Subject: [PATCH 28/42] Switch definition ordering back to original to reduce
 PR diff

---
 src/coq/logicutils/contexts/contextutils.ml | 30 ++++++++++-----------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/coq/logicutils/contexts/contextutils.ml b/src/coq/logicutils/contexts/contextutils.ml
index 104089d..13b9ef9 100644
--- a/src/coq/logicutils/contexts/contextutils.ml
+++ b/src/coq/logicutils/contexts/contextutils.ml
@@ -13,6 +13,21 @@ open Declarations
 
 module CRD = Context.Rel.Declaration
 module CND = Context.Named.Declaration
+
+(* --- Questions about declarations --- *)
+
+(* Is the rel declaration a local assumption? *)
+let is_rel_assum = CRD.is_local_assum
+
+(* Is the rel declaration a local definition? *)
+(* let is_rel_defin x = CRD.is_local_def (get_rel_ctx_name x) *)
+let is_rel_defin x = CRD.is_local_def x
+
+(* Is the named declaration an assumption? *)
+let is_named_assum = CND.is_local_assum
+
+(* Is the named declaration a definition? *)
+let is_named_defin = CND.is_local_def
                        
 (* --- Deconstructing declarations --- *)
 
@@ -34,21 +49,6 @@ let named_value decl = CND.get_value decl
 (* Get the type of a named declaration *)
 let named_type decl = CND.get_type decl
 
-(* --- Questions about declarations --- *)
-
-(* Is the rel declaration a local assumption? *)
-let is_rel_assum = CRD.is_local_assum
-
-(* Is the rel declaration a local definition? *)
-(* let is_rel_defin x = CRD.is_local_def (get_rel_ctx_name x) *)
-let is_rel_defin x = CRD.is_local_def x
-
-(* Is the named declaration an assumption? *)
-let is_named_assum = CND.is_local_assum
-
-(* Is the named declaration a definition? *)
-let is_named_defin = CND.is_local_def
-    
 (* --- Context manipulation tools --- *)
 
 (* Get relative context for a name *)

From b5556224ca36aeb98d0b43bea3c781b7a2a2e113 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Mon, 22 Aug 2022 15:59:07 -0500
Subject: [PATCH 29/42] Remove Proof.compact call

---
 src/coq/decompiler/decompiler.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml
index 98b50fa..4dfdbb7 100644
--- a/src/coq/decompiler/decompiler.ml
+++ b/src/coq/decompiler/decompiler.ml
@@ -38,7 +38,7 @@ let run_tac env sigma (tac : unit Proofview.tactic) (goal : constr)
     : Goal.goal list * Evd.evar_map =
   let p = Proof.start ~name:(destVar goal) ~poly:true sigma [(env, EConstr.of_constr goal)] in
   let (p', _, _) = Proof.run_tactic env tac p in
-  let compact_p = Proof.data (Proof.compact p') in
+  let compact_p = Proof.data p' in
   (compact_p.goals, compact_p.sigma)
 
 (* Returns true if the given tactic solves the goal. *)

From 5d4e2e0b2da687747a055de7fc3ce60c9cadc003 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Mon, 22 Aug 2022 16:57:59 -0500
Subject: [PATCH 30/42] Fix declare_definition call

---
 src/coq/representationutils/defutils.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml
index e683f10..c415393 100644
--- a/src/coq/representationutils/defutils.ml
+++ b/src/coq/representationutils/defutils.ml
@@ -53,7 +53,9 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh =
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   let ubinders = Evd.universe_binders sigma in
   let ce = Declare.definition_entry ?types:tyopt ~univs body in
-  DeclareDef.declare_definition ~name:ident ~scope:(Locality.enforce_locality_exp None Vernacexpr.NoDischarge) ~kind:(Decls.variable_kind ident) ?hook_data:hook ubinders ce imps (* todo: does this even work? *)
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind = Decls.(IsDefinition Definition) in
+  DeclareDef.declare_definition ~name:ident ~scope ~kind ?hook_data:hook ubinders ce imps (* todo: check if we need poly *)
 
 (* Define a new Coq term *)
 let define_term ?typ (n : Id.t) (evm : evar_map) (trm : Constr.types) (refresh : bool) =

From 9b8d5b0a8887b3e6c57e1470757ac9fe5945cf6a Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Tue, 23 Aug 2022 09:16:22 -0500
Subject: [PATCH 31/42] Fix declare_definition bug

---
 src/coq/representationutils/defutils.ml | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml
index c415393..dc8a3fd 100644
--- a/src/coq/representationutils/defutils.ml
+++ b/src/coq/representationutils/defutils.ml
@@ -42,27 +42,19 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh =
     else
       sigma
   in
-  let sigma = Evd.minimize_universes sigma in
-  let body = to_constr sigma body in
-  let tyopt = Option.map (to_constr sigma) tyopt in
-  let uvars_fold uvars c =
-    Univ.LSet.union uvars (Univops.universes_of_constr c) in
-  let uvars = List.fold_left uvars_fold Univ.LSet.empty
-    (Option.List.cons tyopt [body]) in
-  let sigma = Evd.restrict_universe_context sigma uvars in
-  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *)
+  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:tyopt ~body in
   let ubinders = Evd.universe_binders sigma in
-  let ce = Declare.definition_entry ?types:tyopt ~univs body in
   let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
   let kind = Decls.(IsDefinition Definition) in
-  DeclareDef.declare_definition ~name:ident ~scope ~kind ?hook_data:hook ubinders ce imps (* todo: check if we need poly *)
+  DeclareDef.declare_definition ~name:ident ~scope ~kind ?hook_data:hook ubinders ce imps
 
 (* Define a new Coq term *)
 let define_term ?typ (n : Id.t) (evm : evar_map) (trm : Constr.types) (refresh : bool) =
   (* let k = (Global, Flags.is_universe_polymorphism(), Definition) in *)
   let poly = Attributes.is_universe_polymorphism() in
   let udecl = UState.default_univ_decl in
-  (* let nohook = Lemmas.mk_hook (fun _ x -> x) in *)
+  (* let nohook = DeclareDef.Hook.make (fun x -> x) in *)
   let etrm = EConstr.of_constr trm in
   let etyp = Option.map EConstr.of_constr typ in
   edeclare n poly ~opaque:false evm udecl etrm etyp [] None refresh

From e582a0ce34ec094ff859a49b4b6c61fc551efa4b Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Tue, 23 Aug 2022 09:53:41 -0500
Subject: [PATCH 32/42] Add partial implementation of inductive type case

---
 .../logicutils/transformation/transform.ml    | 19 +++++++++++++++++--
 .../logicutils/transformation/transform.mli   |  2 +-
 2 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml
index 83b70dc..1d7268c 100644
--- a/src/coq/logicutils/transformation/transform.ml
+++ b/src/coq/logicutils/transformation/transform.ml
@@ -112,7 +112,7 @@ let try_register_record mod_path (ind, ind') =
  *
  * TODO sigma handling, not sure how to do it here/if we need it
  *)
-let transform_module_structure ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef.Set.empty) ident tr_constr mod_body =
+let transform_module_structure env ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef.Set.empty) ident tr_constr mod_body =
   let open Modutils in
   let mod_path = mod_body.mod_mp in
   let mod_arity, mod_elems = decompose_module_signature mod_body.mod_type in
@@ -142,7 +142,22 @@ let transform_module_structure ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef
         let sigma, const' = transform_constant ident tr_constr const_body in
         GlobRef.Map.add (ConstRef const) (ConstRef const') subst
     | SFBmind mind_body ->
-      Feedback.msg_warning (Pp.str "Mutually inductive types are not supported");
+      check_inductive_supported mind_body;
+      let ind = (MutInd.make2 mod_path label, 0) in
+      let ind_body = mind_body.mind_packets.(0) in
+      let sigma, ind' = transform_inductive ident tr_constr (mind_body, ind_body) in
+      try_register_record mod_path' (ind, ind');
+      let subst = GlobRef.Map.add (IndRef ind) (IndRef ind') subst in
+      (* 
+      let ncons = Array.length ind_body.mind_consnames in
+      let sorts = ind_body.mind_kelim in
+      let list_cons ind = List.init ncons (fun i -> ConstructRef (ind, i + 1)) in
+      let list_elim ind = Indrec.lookup_eliminator env ind sorts in
+      let subst = GlobRef.Map.add (list_cons ind) (list_cons ind') subst in
+      let subst = GlobRef.Map.add (list_elim ind) (list_elim ind') subst in *)
+      (* 
+      List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') |>
+      List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind') *)
       subst
     | SFBmodule mod_body ->
       Feedback.msg_warning (Pp.str "Skipping nested module structure");
diff --git a/src/coq/logicutils/transformation/transform.mli b/src/coq/logicutils/transformation/transform.mli
index 79b32ab..5093e2b 100644
--- a/src/coq/logicutils/transformation/transform.mli
+++ b/src/coq/logicutils/transformation/transform.mli
@@ -45,4 +45,4 @@ val transform_inductive :
  * NOTE: Global side effects.
  *)
 val transform_module_structure :
-  ?init:(unit -> global_substitution) -> ?opaques:(Names.GlobRef.Set.t) -> Id.t -> constr_transformer -> module_body -> ModPath.t
+  env -> ?init:(unit -> global_substitution) -> ?opaques:(Names.GlobRef.Set.t) -> Id.t -> constr_transformer -> module_body -> ModPath.t

From 89efa7855b8d7b6092c2a28e53cfb167e7ec8947 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Wed, 31 Aug 2022 10:22:11 -0500
Subject: [PATCH 33/42] Add fixes

---
 src/coq/logicutils/inductive/indutils.ml      | 29 +++++++++++-
 .../logicutils/transformation/transform.ml    | 47 +++++++++++++++----
 2 files changed, 67 insertions(+), 9 deletions(-)

diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml
index e22310b..6655777 100644
--- a/src/coq/logicutils/inductive/indutils.ml
+++ b/src/coq/logicutils/inductive/indutils.ml
@@ -15,6 +15,8 @@ open Envutils
 open Contextutils
 open Inference
 open Evd
+open Entries
+open DeclareInd
 
 (* Don't support mutually inductive or coinductive types yet (TODO move) *)
 let check_inductive_supported mutind_body : unit =
@@ -196,6 +198,27 @@ let open_inductive ?(global=false) env (mind_body, ind_body) =
   let ctors_typ = Array.map (recompose_prod_assum arity_ctx) ind_body.mind_user_lc in
   env, univs, subst_univs arity, Array.map_to_list subst_univs ctors_typ
 
+
+(* Internal func from the Coq kernel, for debugging. This func used to be exposed, but now is hidden.
+   TODO: remove 
+let declare_mind mie =
+  let id = match mie.mind_entry_inds with
+  | ind::_ -> ind.mind_entry_typename
+  | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
+  let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in
+  let names = List.map map_names mie.mind_entry_inds in
+  List.iter (fun (typ, cons) -> Declare.check_exists typ;
+  List.iter Declare.check_exists cons) names;
+  let _kn' = Global.add_mind id mie in
+  let (sp,kn as oname) = Lib.add_leaf id (DeclareInd.inInductive { ind_names = names }) in
+  if is_unsafe_typing_flags() then feedback_axiom ();
+  let mind = Global.mind_of_delta_kn kn in
+  let isprim = declare_projections mie.mind_entry_universes mind in
+  Impargs.declare_mib_implicits mind;
+  declare_inductive_argument_scopes mind mie;
+  oname, isprim
+*)
+
 let declare_inductive typename consnames template univs nparam arity constypes =
   let open Entries in
   let params, arity = Term.decompose_prod_n_assum nparam arity in
@@ -217,7 +240,11 @@ let declare_inductive typename consnames template univs nparam arity constypes =
       mind_entry_private = None }
   in
   let mind = DeclareInd.declare_mutual_inductive_with_eliminations mind_entry UnivNames.empty_binders [] in
-  (* let mind = MutInd.make1 ker_name in *)
+  (mind, 0)
+  (* 
+  let ((_, ker_name), _) = declare_mind mind_entry in
+  let mind = MutInd.make1 ker_name in
   let ind = (mind, 0) in
   Indschemes.declare_default_schemes mind;
   ind
+  *)
diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml
index 1d7268c..c315736 100644
--- a/src/coq/logicutils/transformation/transform.ml
+++ b/src/coq/logicutils/transformation/transform.ml
@@ -16,6 +16,7 @@ open Substitution
 open Stateutils
 open Recordops
 open Record
+open Printing
 
 (* Type-sensitive transformation of terms *)
 type constr_transformer = env -> evar_map -> constr -> evar_map * constr
@@ -54,6 +55,7 @@ let transform_constant ident tr_constr const_body =
   let sigma = Evd.from_env env in
   let sigma, term' = tr_constr env sigma term in
   let sigma, type' = tr_constr env sigma const_body.const_type in
+  let open Printing in
   sigma, Globnames.destConstRef (define_term ~typ:type' ident sigma term' true)
 
 (*
@@ -98,6 +100,18 @@ let try_register_record mod_path (ind, ind') =
   with Not_found ->
     ()
 
+let lookup_eliminator_error_handling ind sorts = 
+  let env = Global.env () in
+  List.filter_map (fun x -> x)
+  (List.map 
+    (fun x -> 
+      Feedback.msg_warning (Sorts.pr_sort_family (x));
+      try Some (Indrec.lookup_eliminator env ind x)
+      with
+      | _ -> None
+    )
+    sorts)
+
 (*
  * Declare a new module structure under the given name with the compositionally
  * transformed (i.e., forward-substituted) components from the given module
@@ -148,17 +162,34 @@ let transform_module_structure env ?(init=const GlobRef.Map.empty) ?(opaques=Glo
       let sigma, ind' = transform_inductive ident tr_constr (mind_body, ind_body) in
       try_register_record mod_path' (ind, ind');
       let subst = GlobRef.Map.add (IndRef ind) (IndRef ind') subst in
-      (* 
       let ncons = Array.length ind_body.mind_consnames in
-      let sorts = ind_body.mind_kelim in
       let list_cons ind = List.init ncons (fun i -> ConstructRef (ind, i + 1)) in
-      let list_elim ind = Indrec.lookup_eliminator env ind sorts in
-      let subst = GlobRef.Map.add (list_cons ind) (list_cons ind') subst in
-      let subst = GlobRef.Map.add (list_elim ind) (list_elim ind') subst in *)
-      (* 
+      (* let sorts = List.map Sorts.family [Sorts.sprop; Sorts.set; Sorts.prop; Sorts.type1] in *)
+      let sorts = List.map Sorts.family [Sorts.sprop; Sorts.prop; Sorts.set; Sorts.type1] in
+      let list_elim ind_arg = lookup_eliminator_error_handling ind_arg sorts in
+      Feedback.msg_warning (Names.MutInd.print (fst ind));
+      Feedback.msg_warning (Pp.str ("ind level " ^ (string_of_int (snd ind))));
+      Feedback.msg_warning (Names.MutInd.print (fst ind'));
+      Feedback.msg_warning (Pp.str ("ind level " ^ (string_of_int (snd ind'))));
+      Feedback.msg_warning (Pp.str (string_of_int (List.length (list_cons ind))));
+      Feedback.msg_warning (Pp.str (string_of_int (List.length (list_elim ind))));
+      Feedback.msg_warning (Pp.str (string_of_int (List.length (list_cons ind'))));
+      Feedback.msg_warning (Pp.str (string_of_int (List.length (list_elim ind'))));
+      GlobRef.Map.add (IndRef ind) (IndRef ind') subst |>
       List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') |>
-      List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind') *)
-      subst
+      List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind')
+      (* let sorts = List.map (fun x -> x ind_body.mind_kelim) sort_funcs in *)
+      (* let sorts = List.filter (fun x -> match Sorts.relevance_of_sort_family x with 
+                                        | Sorts.Relevant -> true
+                                        | Sorts.Irrelevant -> false 
+                              )  *)
+      (* List.filter (fun x -> Sorts.family_leq x ind_body.mind_kelim) *)
+      (* Feedback.msg_warning (Pp.str (string_of_int (List.length sorts))); *)
+      (*
+      let subst = GlobRef.Map.add (IndRef ind) (IndRef ind') subst in 
+      let subst = List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') subst in
+      let subst = List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind') subst in 
+      subst *)
     | SFBmodule mod_body ->
       Feedback.msg_warning (Pp.str "Skipping nested module structure");
       subst

From 3a593472516d866b629e63680c2cbdb1b76778fa Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Tue, 27 Sep 2022 10:54:43 -0500
Subject: [PATCH 34/42] Attempt to fix list_elim bug

---
 .../logicutils/transformation/transform.ml    | 30 +++++++++++++++----
 1 file changed, 25 insertions(+), 5 deletions(-)

diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml
index c315736..e46a240 100644
--- a/src/coq/logicutils/transformation/transform.ml
+++ b/src/coq/logicutils/transformation/transform.ml
@@ -4,6 +4,8 @@
  * TODO move out some module stuff etc.
  *)
 
+(* open Stdlib
+open Map *)
 open Util
 open Environ
 open Constr
@@ -101,12 +103,13 @@ let try_register_record mod_path (ind, ind') =
     ()
 
 let lookup_eliminator_error_handling ind sorts = 
+  Feedback.msg_warning (Pp.(str "start "));
   let env = Global.env () in
   List.filter_map (fun x -> x)
   (List.map 
     (fun x -> 
-      Feedback.msg_warning (Sorts.pr_sort_family (x));
-      try Some (Indrec.lookup_eliminator env ind x)
+      (* try Some (x, Indrec.lookup_eliminator env ind x) *)
+      try Some (x, Indrec.lookup_eliminator env ind x)
       with
       | _ -> None
     )
@@ -167,6 +170,17 @@ let transform_module_structure env ?(init=const GlobRef.Map.empty) ?(opaques=Glo
       (* let sorts = List.map Sorts.family [Sorts.sprop; Sorts.set; Sorts.prop; Sorts.type1] in *)
       let sorts = List.map Sorts.family [Sorts.sprop; Sorts.prop; Sorts.set; Sorts.type1] in
       let list_elim ind_arg = lookup_eliminator_error_handling ind_arg sorts in
+
+      let list_elim_ind = list_elim ind in
+      let list_elim_ind' = list_elim ind' in
+      let list_elim_ind_map = Map.S.of_seq list_elim_ind in 
+      let list_elim_ind'_map = Map.S.of_seq list_elim_ind' in 
+      let list_elim_ind_sorts = Set.S.of_seq (fst (unzip list_elim_ind)) in
+      let list_elim_ind'_sorts = Set.S.of_seq (fst (unzip list_elim_ind')) in
+      let common_sorts = inter (list_elim_ind_sorts list_elim_ind'_sorts) in 
+      let list_elim_ind_winnowed = Map.S.filter (fun x -> Set.S.mem x common_sort) list_elim_ind_map in
+      let list_elim_ind'_winnowed = Map.S.filter (fun x -> Set.S.mem x common_sort) list_elim_ind'_map in
+      (*
       Feedback.msg_warning (Names.MutInd.print (fst ind));
       Feedback.msg_warning (Pp.str ("ind level " ^ (string_of_int (snd ind))));
       Feedback.msg_warning (Names.MutInd.print (fst ind'));
@@ -175,9 +189,7 @@ let transform_module_structure env ?(init=const GlobRef.Map.empty) ?(opaques=Glo
       Feedback.msg_warning (Pp.str (string_of_int (List.length (list_elim ind))));
       Feedback.msg_warning (Pp.str (string_of_int (List.length (list_cons ind'))));
       Feedback.msg_warning (Pp.str (string_of_int (List.length (list_elim ind'))));
-      GlobRef.Map.add (IndRef ind) (IndRef ind') subst |>
-      List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') |>
-      List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind')
+      *)
       (* let sorts = List.map (fun x -> x ind_body.mind_kelim) sort_funcs in *)
       (* let sorts = List.filter (fun x -> match Sorts.relevance_of_sort_family x with 
                                         | Sorts.Relevant -> true
@@ -190,6 +202,14 @@ let transform_module_structure env ?(init=const GlobRef.Map.empty) ?(opaques=Glo
       let subst = List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') subst in
       let subst = List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind') subst in 
       subst *)
+      (*
+      GlobRef.Map.add (IndRef ind) (IndRef ind') subst |>
+      List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') |>
+      List.fold_right2 GlobRef.Map.add (list_elim ind) (list_elim ind')
+      *)
+      GlobRef.Map.add (IndRef ind) (IndRef ind') subst |>
+      List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') |>
+      List.fold_right2 GlobRef.Map.add (list_elim_ind_winnowed) (list_elim_ind'_winnowed)
     | SFBmodule mod_body ->
       Feedback.msg_warning (Pp.str "Skipping nested module structure");
       subst

From 0e9cb9bad826acfbf43100298c4a58a9a8b8b049 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Tue, 27 Sep 2022 11:19:51 -0500
Subject: [PATCH 35/42] Finish fixing list_elim bug; todo: refactor and clean
 up

---
 src/coq/logicutils/transformation/transform.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml
index e46a240..2192e59 100644
--- a/src/coq/logicutils/transformation/transform.ml
+++ b/src/coq/logicutils/transformation/transform.ml
@@ -4,8 +4,8 @@
  * TODO move out some module stuff etc.
  *)
 
-(* open Stdlib
-open Map *)
+open Stdlib
+open Map
 open Util
 open Environ
 open Constr
@@ -173,13 +173,13 @@ let transform_module_structure env ?(init=const GlobRef.Map.empty) ?(opaques=Glo
 
       let list_elim_ind = list_elim ind in
       let list_elim_ind' = list_elim ind' in
-      let list_elim_ind_map = Map.S.of_seq list_elim_ind in 
-      let list_elim_ind'_map = Map.S.of_seq list_elim_ind' in 
-      let list_elim_ind_sorts = Set.S.of_seq (fst (unzip list_elim_ind)) in
-      let list_elim_ind'_sorts = Set.S.of_seq (fst (unzip list_elim_ind')) in
-      let common_sorts = inter (list_elim_ind_sorts list_elim_ind'_sorts) in 
-      let list_elim_ind_winnowed = Map.S.filter (fun x -> Set.S.mem x common_sort) list_elim_ind_map in
-      let list_elim_ind'_winnowed = Map.S.filter (fun x -> Set.S.mem x common_sort) list_elim_ind'_map in
+      (* let list_elim_ind_map = Map.Make.of_seq list_elim_ind in 
+      let list_elim_ind'_map = Map.Make.of_seq list_elim_ind' in *)
+      let list_elim_ind_sorts = List.map fst list_elim_ind in
+      let list_elim_ind'_sorts = List.map fst list_elim_ind' in
+      let common_sorts = List.filter (fun x -> List.exists (fun y -> Sorts.family_equal x y) list_elim_ind_sorts) list_elim_ind'_sorts in 
+      let list_elim_ind_winnowed = List.map snd (List.filter (fun (x, y) -> List.exists (fun z -> Sorts.family_equal x z) common_sorts) list_elim_ind) in
+      let list_elim_ind'_winnowed = List.map snd (List.filter (fun (x, y) -> List.exists (fun z -> Sorts.family_equal x z) common_sorts) list_elim_ind') in
       (*
       Feedback.msg_warning (Names.MutInd.print (fst ind));
       Feedback.msg_warning (Pp.str ("ind level " ^ (string_of_int (snd ind))));

From 966f8d4db1076abaed670b3d93a8002098a2a12d Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Tue, 27 Sep 2022 14:29:07 -0500
Subject: [PATCH 36/42] Comment out debugging statement

---
 Makefile                                      | 828 ++++++++++++++++++
 Makefile.conf                                 |  54 ++
 src/coq/logicutils/inductive/.indutils.ml.swp | Bin 0 -> 28672 bytes
 .../logicutils/inductive/.indutils.mli.swp    | Bin 0 -> 12288 bytes
 .../transformation/.transform.ml.swp          | Bin 0 -> 28672 bytes
 .../logicutils/transformation/transform.ml    |   2 +-
 6 files changed, 883 insertions(+), 1 deletion(-)
 create mode 100644 Makefile
 create mode 100644 Makefile.conf
 create mode 100644 src/coq/logicutils/inductive/.indutils.ml.swp
 create mode 100644 src/coq/logicutils/inductive/.indutils.mli.swp
 create mode 100644 src/coq/logicutils/transformation/.transform.ml.swp

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..c786ebd
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,828 @@
+###############################################################################
+##  v      #                   The Coq Proof Assistant                       ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                   ##
+##   \VV/  #                                                                 ##
+##    //   #                                                                 ##
+###############################################################################
+## GNUMakefile for Coq 8.11.1
+
+# For debugging purposes (must stay here, don't move below)
+INITIAL_VARS := $(.VARIABLES)
+# To implement recursion we save the name of the main Makefile
+SELF := $(lastword $(MAKEFILE_LIST))
+PARENT := $(firstword $(MAKEFILE_LIST))
+
+# This file is generated by coq_makefile and contains many variable
+# definitions, like the list of .v files or the path to Coq
+include Makefile.conf
+
+# Put in place old names
+VFILES            := $(COQMF_VFILES)
+MLIFILES          := $(COQMF_MLIFILES)
+MLFILES           := $(COQMF_MLFILES)
+MLGFILES          := $(COQMF_MLGFILES)
+MLPACKFILES       := $(COQMF_MLPACKFILES)
+MLLIBFILES        := $(COQMF_MLLIBFILES)
+CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
+INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
+OTHERFLAGS        := $(COQMF_OTHERFLAGS)
+COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
+OCAMLLIBS         := $(COQMF_OCAMLLIBS)
+SRC_SUBDIRS       := $(COQMF_SRC_SUBDIRS)
+COQLIBS           := $(COQMF_COQLIBS)
+COQLIBS_NOML      := $(COQMF_COQLIBS_NOML)
+CMDLINE_COQLIBS   := $(COQMF_CMDLINE_COQLIBS)
+LOCAL             := $(COQMF_LOCAL)
+COQLIB            := $(COQMF_COQLIB)
+DOCDIR            := $(COQMF_DOCDIR)
+OCAMLFIND         := $(COQMF_OCAMLFIND)
+CAMLFLAGS         := $(COQMF_CAMLFLAGS)
+HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
+OCAMLWARN         := $(COQMF_WARN)
+
+Makefile.conf: _CoqProject
+	coq_makefile -f _CoqProject -o Makefile
+
+# This file can be created by the user to hook into double colon rules or
+# add any other Makefile code he may need
+-include Makefile.local
+
+# Parameters ##################################################################
+#
+# Parameters are make variable assignments.
+# They can be passed to (each call to) make on the command line.
+# They can also be put in Makefile.local once an for all.
+# For retro-compatibility reasons they can be put in the _CoqProject, but this
+# practice is discouraged since _CoqProject better not contain make specific
+# code (be nice to user interfaces).
+
+# Print shell commands (set to non empty)
+VERBOSE ?=
+
+# Time the Coq process (set to non empty), and how (see default value)
+TIMED?=
+TIMECMD?=
+# Use command time on linux, gtime on Mac OS
+TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+ifneq (,$(TIMED))
+ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=command time -f $(TIMEFMT)
+else
+ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=gtime -f $(TIMEFMT)
+else
+STDTIME?=command time
+endif
+endif
+else
+STDTIME?=command time -f $(TIMEFMT)
+endif
+
+ifneq (,$(COQBIN))
+# add an ending /
+COQBIN:=$(COQBIN)/
+endif
+
+# Coq binaries
+COQC     ?= "$(COQBIN)coqc"
+COQTOP   ?= "$(COQBIN)coqtop"
+COQCHK   ?= "$(COQBIN)coqchk"
+COQDEP   ?= "$(COQBIN)coqdep"
+COQDOC   ?= "$(COQBIN)coqdoc"
+COQPP    ?= "$(COQBIN)coqpp"
+COQMKFILE ?= "$(COQBIN)coq_makefile"
+
+# Timing scripts
+COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
+COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
+BEFORE ?=
+AFTER ?=
+
+# FIXME this should be generated by Coq (modules already linked by Coq)
+CAMLDONTLINK=unix,str
+
+# OCaml binaries
+CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
+CAMLOPTC    ?= "$(OCAMLFIND)" opt      -c
+CAMLLINK    ?= "$(OCAMLFIND)" ocamlc   -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLOPTLINK ?= "$(OCAMLFIND)" opt      -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLDOC     ?= "$(OCAMLFIND)" ocamldoc
+CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack
+
+# DESTDIR is prepended to all installation paths
+DESTDIR ?=
+
+# Debug builds, typically -g to OCaml, -debug to Coq.
+CAMLDEBUG ?=
+COQDEBUG ?=
+
+# Extra packages to be linked in (as in findlib -package)
+CAMLPKGS ?=
+
+# Option for making timing files
+TIMING?=
+# Option for changing sorting of timing output file
+TIMING_SORT_BY ?= auto
+# Output file names for timed builds
+TIME_OF_BUILD_FILE               ?= time-of-build.log
+TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
+TIME_OF_BUILD_AFTER_FILE         ?= time-of-build-after.log
+TIME_OF_PRETTY_BUILD_FILE        ?= time-of-build-pretty.log
+TIME_OF_PRETTY_BOTH_BUILD_FILE   ?= time-of-build-both.log
+TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
+
+TGTS ?=
+
+########## End of parameters ##################################################
+# What follows may be relevant to you only if you need to
+# extend this Makefile.  If so, look for 'Extension point' here and
+# put in Makefile.local double colon rules accordingly.
+# E.g. to perform some work after the all target completes you can write
+#
+# post-all::
+# 	echo "All done!"
+#
+# in Makefile.local
+#
+###############################################################################
+
+
+
+
+# Flags #######################################################################
+#
+# We define a bunch of variables combining the parameters.
+# To add additional flags to coq, coqchk or coqdoc, set the
+# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add.
+# To overwrite the default choice and set your own flags entirely, set the
+# {COQ,COQCHK,COQDOC}FLAGS variable.
+
+SHOW := $(if $(VERBOSE),@true "",@echo "")
+HIDE := $(if $(VERBOSE),,@)
+
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
+
+OPT?=
+
+# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
+ifeq '$(OPT)' '-byte'
+USEBYTE:=true
+DYNOBJ:=.cma
+DYNLIB:=.cma
+else
+USEBYTE:=
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
+endif
+
+# these variables are meant to be overridden if you want to add *extra* flags
+COQEXTRAFLAGS?=
+COQCHKEXTRAFLAGS?=
+COQDOCEXTRAFLAGS?=
+
+# these flags do NOT contain the libraries, to make them easier to overwrite
+COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS)
+COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
+COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS)
+
+COQDOCLIBS?=$(COQLIBS_NOML)
+
+# The version of Coq being run and the version of coq_makefile that
+# generated this makefile
+COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
+COQMAKEFILE_VERSION:=8.11.1
+
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
+
+CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
+# ocamldoc fails with unknown argument otherwise
+CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLFLAGS+=$(OCAMLWARN)
+
+ifneq (,$(TIMING))
+TIMING_ARG=-time
+ifeq (after,$(TIMING))
+TIMING_EXT=after-timing
+else
+ifeq (before,$(TIMING))
+TIMING_EXT=before-timing
+else
+TIMING_EXT=timing
+endif
+endif
+else
+TIMING_ARG=
+endif
+
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
+endif
+
+concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
+
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
+
+# Files #######################################################################
+#
+# We here define a bunch of variables about the files being part of the
+# Coq project in order to ease the writing of build target and build rules
+
+VDFILE := .Makefile.d
+
+ALLSRCFILES := \
+	$(MLGFILES) \
+	$(MLFILES) \
+	$(MLPACKFILES) \
+	$(MLLIBFILES) \
+	$(MLIFILES)
+
+# helpers
+vo_to_obj = $(addsuffix .o,\
+  $(filter-out Warning: Error:,\
+  $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1))))
+strip_dotslash = $(patsubst ./%,%,$(1))
+
+# without this we get undefined variables in the expansion for the
+# targets of the [deprecated,use-mllib-or-mlpack] rule
+with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1)))
+
+VO = vo
+VOS = vos
+
+VOFILES = $(VFILES:.v=.$(VO))
+GLOBFILES = $(VFILES:.v=.glob)
+HTMLFILES = $(VFILES:.v=.html)
+GHTMLFILES = $(VFILES:.v=.g.html)
+BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
+TEXFILES = $(VFILES:.v=.tex)
+GTEXFILES = $(VFILES:.v=.g.tex)
+CMOFILES = \
+	$(MLGFILES:.mlg=.cmo) \
+	$(MLFILES:.ml=.cmo) \
+	$(MLPACKFILES:.mlpack=.cmo)
+CMXFILES = $(CMOFILES:.cmo=.cmx)
+OFILES = $(CMXFILES:.cmx=.o)
+CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma)
+CMXAFILES = $(CMAFILES:.cma=.cmxa)
+CMIFILES = \
+	$(CMOFILES:.cmo=.cmi) \
+	$(MLIFILES:.mli=.cmi)
+# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
+# a .mlg file
+CMXSFILES = \
+	$(MLPACKFILES:.mlpack=.cmxs) \
+	$(CMXAFILES:.cmxa=.cmxs) \
+	$(if $(MLPACKFILES)$(CMXAFILES),,\
+		$(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs))
+
+# files that are packed into a plugin (no extension)
+PACKEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+	    $(call strip_dotslash, \
+	       $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib))))
+# files that are archived into a .cma (mllib)
+LIBEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+	    $(call strip_dotslash, \
+	       $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib))))
+CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES))
+CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
+OBJFILES = $(call vo_to_obj,$(VOFILES))
+ALLNATIVEFILES = \
+	$(OBJFILES:.o=.cmi) \
+	$(OBJFILES:.o=.cmx) \
+	$(OBJFILES:.o=.cmxs)
+# trick: wildcard filters out non-existing files, so that `install` doesn't show
+# warnings and `clean` doesn't pass to rm a list of files that is too long for
+# the shell.
+NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
+FILESTOINSTALL = \
+	$(VOFILES) \
+	$(VFILES) \
+	$(GLOBFILES) \
+	$(NATIVEFILES) \
+	$(CMIFILESTOINSTALL)
+BYTEFILESTOINSTALL = \
+	$(CMOFILESTOINSTALL) \
+	$(CMAFILES)
+ifeq '$(HASNATDYNLINK)' 'true'
+DO_NATDYNLINK = yes
+FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
+else
+DO_NATDYNLINK =
+endif
+
+ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE)
+
+# Compilation targets #########################################################
+
+all:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
+.PHONY: all
+
+all.timing.diff:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES=""
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
+.PHONY: all.timing.diff
+
+make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
+make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
+make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
+	$(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
+print-pretty-timed::
+	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+print-pretty-timed-diff::
+	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ifeq (,$(BEFORE))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
+	$(HIDE)false
+else
+ifeq (,$(AFTER))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
+	$(HIDE)false
+else
+print-pretty-single-time-diff::
+	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+endif
+endif
+pretty-timed:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed
+.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff
+
+# Extension points for actions to be performed before/after the all target
+pre-all::
+	@# Extension point
+	$(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
+	  echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
+	  echo "W: while the current Coq version is $(COQ_VERSION)";\
+	fi
+.PHONY: pre-all
+
+post-all::
+	@# Extension point
+.PHONY: post-all
+
+real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
+.PHONY: real-all
+
+real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff)
+.PHONY: real-all.timing.diff
+
+bytefiles: $(CMOFILES) $(CMAFILES)
+.PHONY: bytefiles
+
+optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
+.PHONY: optfiles
+
+# FIXME, see Ralf's bugreport
+# quick is deprecated, now renamed vio
+vio: $(VOFILES:.vo=.vio)
+.PHONY: vio
+quick: vio
+	$(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files")
+.PHONY: quick
+
+vio2vo:
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
+		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: vio2vo
+
+# quick2vo is undocumented
+quick2vo:
+	$(HIDE)make -j $(J) vio
+	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
+	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
+	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
+	done); \
+	echo "VIO2VO: $$VIOFILES"; \
+	if [ -n "$$VIOFILES" ]; then \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
+	fi
+.PHONY: quick2vo
+
+checkproofs:
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
+		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: checkproofs
+
+vos: $(VOFILES:%.vo=%.vos)
+.PHONY: vos
+
+vok: $(VOFILES:%.vo=%.vok)
+.PHONY: vok
+
+validate: $(VOFILES)
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
+.PHONY: validate
+
+only: $(TGTS)
+.PHONY: only
+
+# Documentation targets #######################################################
+
+html: $(GLOBFILES) $(VFILES)
+	$(SHOW)'COQDOC -d html $(GAL)'
+	$(HIDE)mkdir -p html
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
+
+mlihtml: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'CAMLDOC -d $@'
+	$(HIDE)mkdir $@ || rm -rf $@/*
+	$(HIDE)$(CAMLDOC) -html \
+		-d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
+
+all-mli.tex: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'CAMLDOC -latex $@'
+	$(HIDE)$(CAMLDOC) -latex \
+		-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
+
+all.ps: $(VFILES)
+	$(SHOW)'COQDOC -ps $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all.pdf: $(VFILES)
+	$(SHOW)'COQDOC -pdf $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+# FIXME: not quite right, since the output name is different
+gallinahtml: GAL=-g
+gallinahtml: html
+
+all-gal.ps: GAL=-g
+all-gal.ps: all.ps
+
+all-gal.pdf: GAL=-g
+all-gal.pdf: all.pdf
+
+# ?
+beautify: $(BEAUTYFILES)
+	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+	@echo 'Do not do "make clean" until you are sure that everything went well!'
+	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+.PHONY: beautify
+
+# Installation targets ########################################################
+#
+# There rules can be extended in Makefile.local
+# Extensions can't assume when they run.
+
+install:
+	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
+	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
+	done; exit $$code
+	$(HIDE)for f in $(FILESTOINSTALL); do\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+	$(HIDE)$(MAKE) install-extra -f "$(SELF)"
+install-extra::
+	@# Extension point
+.PHONY: install install-extra
+
+install-byte:
+	$(HIDE)for f in $(BYTEFILESTOINSTALL); do\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+
+install-doc:: html mlihtml
+	@# Extension point
+	$(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(HIDE)for i in html/*; do \
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
+	done
+	$(HIDE)install -d \
+		"$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE)for i in mlihtml/*; do \
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
+	done
+.PHONY: install-doc
+
+uninstall::
+	@# Extension point
+	$(HIDE)for f in $(FILESTOINSTALL); do \
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
+	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
+	 rm -f "$$instf" &&\
+	 echo RM "$$instf" &&\
+	 (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+	done
+.PHONY: uninstall
+
+uninstall-doc::
+	@# Extension point
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
+.PHONY: uninstall-doc
+
+# Cleaning ####################################################################
+#
+# There rules can be extended in Makefile.local
+# Extensions can't assume when they run.
+
+clean::
+	@# Extension point
+	$(SHOW)'CLEAN'
+	$(HIDE)rm -f $(CMOFILES)
+	$(HIDE)rm -f $(CMIFILES)
+	$(HIDE)rm -f $(CMAFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
+	$(HIDE)rm -f $(CMXAFILES)
+	$(HIDE)rm -f $(CMXSFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
+	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
+	$(HIDE)rm -f $(MLGFILES:.mlg=.ml)
+	$(HIDE)rm -f $(ALLDFILES)
+	$(HIDE)rm -f $(NATIVEFILES)
+	$(HIDE)find . -name .coq-native -type d -empty -delete
+	$(HIDE)rm -f $(VOFILES)
+	$(HIDE)rm -f $(VOFILES:.vo=.vio)
+	$(HIDE)rm -f $(VOFILES:.vo=.vos)
+	$(HIDE)rm -f $(VOFILES:.vo=.vok)
+	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
+	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
+	$(HIDE)rm -f $(VFILES:.v=.glob)
+	$(HIDE)rm -f $(VFILES:.v=.tex)
+	$(HIDE)rm -f $(VFILES:.v=.g.tex)
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)rm -rf html mlihtml
+.PHONY: clean
+
+cleanall:: clean
+	@# Extension point
+	$(SHOW)'CLEAN *.aux *.timing'
+	$(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+	$(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.before-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.after-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff)
+.PHONY: cleanall
+
+archclean::
+	@# Extension point
+	$(SHOW)'CLEAN *.cmx *.o'
+	$(HIDE)rm -f $(NATIVEFILES)
+	$(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
+.PHONY: archclean
+
+
+# Compilation rules ###########################################################
+
+$(MLIFILES:.mli=.cmi): %.cmi: %.mli
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+
+$(MLGFILES:.mlg=.ml): %.ml: %.mlg
+	$(SHOW)'COQPP $<'
+	$(HIDE)$(COQPP) $<
+
+# Stupid hack around a deficient syntax: we cannot concatenate two expansions
+$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+
+# Same hack
+$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
+	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
+
+
+$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-linkall -shared -o $@ $<
+
+$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+
+
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -linkall -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
+	$(SHOW)'CAMLC -pack -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
+	$(SHOW)'CAMLOPT -pack -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+# This rule is for _CoqProject with no .mllib nor .mlpack
+$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
+	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -o $@ $<
+
+ifneq (,$(TIMING))
+TIMING_EXTRA = > $<.$(TIMING_EXT)
+else
+TIMING_EXTRA =
+endif
+
+$(VOFILES): %.vo: %.v
+	$(SHOW)COQC $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
+
+# FIXME ?merge with .vo / .vio ?
+$(GLOBFILES): %.glob: %.v
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+
+$(VFILES:.v=.vio): %.vio: %.v
+	$(SHOW)COQC -vio $<
+	$(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+
+$(VFILES:.v=.vos): %.vos: %.v
+	$(SHOW)COQC -vos $<
+	$(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+
+$(VFILES:.v=.vok): %.vok: %.v
+	$(SHOW)COQC -vok $<
+	$(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+
+$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
+	$(SHOW)PYTHON TIMING-DIFF $<
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
+
+$(BEAUTYFILES): %.v.beautified: %.v
+	$(SHOW)'BEAUTIFY $<'
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
+
+$(TEXFILES): %.tex: %.v
+	$(SHOW)'COQDOC -latex $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+$(GTEXFILES): %.g.tex: %.v
+	$(SHOW)'COQDOC -latex -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+$(HTMLFILES): %.html: %.v %.glob
+	$(SHOW)'COQDOC -html $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+$(GHTMLFILES): %.g.html: %.v %.glob
+	$(SHOW)'COQDOC -html -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
+
+# Dependency files ############################################################
+
+ifndef MAKECMDGOALS
+  -include $(ALLDFILES)
+else
+  ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
+   -include $(ALLDFILES)
+ endif
+endif
+
+.SECONDARY: $(ALLDFILES)
+
+redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV )
+
+GENMLFILES:=$(MLGFILES:.mlg=.ml)
+$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES)
+
+$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+# If this makefile is created using a _CoqProject we have coqdep get
+# options from it. This avoids argument length limits for pathological
+# projects. Note that extra options might be on the command line.
+VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
+
+$(VDFILE): $(VFILES)
+	$(SHOW)'COQDEP VFILES'
+	$(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+
+# Misc ########################################################################
+
+byte:
+	$(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)"
+.PHONY: byte
+
+opt:
+	$(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
+.PHONY:	opt
+
+# This is deprecated.  To extend this makefile use
+# extension points and Makefile.local
+printenv::
+	$(warning printenv is deprecated)
+	$(warning write extensions in Makefile.local or include Makefile.conf)
+	@echo 'LOCAL = $(LOCAL)'
+	@echo 'COQLIB = $(COQLIB)'
+	@echo 'DOCDIR = $(DOCDIR)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
+	@echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)'
+	@echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'PP = $(PP)'
+	@echo 'COQFLAGS = $(COQFLAGS)'
+	@echo 'COQLIB = $(COQLIBS)'
+	@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
+.PHONY:	printenv
+
+# Generate a .merlin file.  If you need to append directives to this
+# file you can extend the merlin-hook target in Makefile.local
+.merlin:
+	$(SHOW)'FILL .merlin'
+	$(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
+	$(HIDE)echo 'B $(COQLIB)' >> .merlin
+	$(HIDE)echo 'S $(COQLIB)' >> .merlin
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo 'B $(COQLIB)$(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo 'S $(COQLIB)$(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;)
+	$(HIDE)$(MAKE) merlin-hook -f "$(SELF)"
+.PHONY: merlin
+
+merlin-hook::
+	@# Extension point
+.PHONY: merlin-hook
+
+# prints all variables
+debug:
+	$(foreach v,\
+		$(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\
+	       		$(.VARIABLES))),\
+	       	$(info $(v) = $($(v))))
+.PHONY: debug
+
+.DEFAULT_GOAL := all
+
+# Local Variables:
+# mode: makefile-gmake
+# End:
diff --git a/Makefile.conf b/Makefile.conf
new file mode 100644
index 0000000..a41d6b4
--- /dev/null
+++ b/Makefile.conf
@@ -0,0 +1,54 @@
+# This configuration file was generated by running:
+# coq_makefile -f _CoqProject -o Makefile
+
+
+###############################################################################
+#                                                                             #
+# Project files.                                                              #
+#                                                                             #
+###############################################################################
+
+COQMF_VFILES = theories/Plib.v
+COQMF_MLIFILES = src/utilities/utilities.mli src/coq/termutils/apputils.mli src/coq/termutils/constutils.mli src/coq/termutils/funutils.mli src/coq/representationutils/defutils.mli src/coq/representationutils/nameutils.mli src/coq/logicutils/typesandequality/inference.mli src/coq/logicutils/typesandequality/convertibility.mli src/coq/logicutils/typesandequality/checking.mli src/coq/constants/equtils.mli src/coq/constants/sigmautils.mli src/coq/constants/produtils.mli src/coq/constants/idutils.mli src/coq/constants/proputils.mli src/coq/logicutils/contexts/stateutils.mli src/coq/logicutils/contexts/envutils.mli src/coq/logicutils/contexts/contextutils.mli src/coq/logicutils/hofs/hofs.mli src/coq/logicutils/hofs/hofimpls.mli src/coq/logicutils/hofs/debruijn.mli src/coq/logicutils/hofs/substitution.mli src/coq/logicutils/hofs/reducers.mli src/coq/logicutils/hofs/typehofs.mli src/coq/logicutils/hofs/zooming.mli src/coq/logicutils/hofs/hypotheses.mli src/coq/logicutils/hofs/filters.mli src/coq/logicutils/inductive/indexing.mli src/coq/logicutils/inductive/indutils.mli src/coq/logicutils/contexts/modutils.mli src/coq/logicutils/transformation/transform.mli src/coq/devutils/printing.mli src/coq/decompiler/decompiler.mli
+COQMF_MLFILES = src/utilities/utilities.ml src/coq/termutils/apputils.ml src/coq/termutils/constutils.ml src/coq/termutils/funutils.ml src/coq/representationutils/defutils.ml src/coq/representationutils/nameutils.ml src/coq/logicutils/typesandequality/inference.ml src/coq/logicutils/typesandequality/convertibility.ml src/coq/logicutils/typesandequality/checking.ml src/coq/constants/equtils.ml src/coq/constants/sigmautils.ml src/coq/constants/produtils.ml src/coq/constants/idutils.ml src/coq/constants/proputils.ml src/coq/logicutils/contexts/stateutils.ml src/coq/logicutils/contexts/envutils.ml src/coq/logicutils/contexts/contextutils.ml src/coq/logicutils/hofs/hofs.ml src/coq/logicutils/hofs/hofimpls.ml src/coq/logicutils/hofs/debruijn.ml src/coq/logicutils/hofs/substitution.ml src/coq/logicutils/hofs/reducers.ml src/coq/logicutils/hofs/typehofs.ml src/coq/logicutils/hofs/zooming.ml src/coq/logicutils/hofs/hypotheses.ml src/coq/logicutils/hofs/filters.ml src/coq/logicutils/inductive/indexing.ml src/coq/logicutils/inductive/indutils.ml src/coq/logicutils/contexts/modutils.ml src/coq/logicutils/transformation/transform.ml src/coq/devutils/printing.ml src/coq/decompiler/decompiler.ml
+COQMF_MLGFILES = src/plibrary.mlg
+COQMF_MLPACKFILES = src/plib.mlpack
+COQMF_MLLIBFILES = 
+COQMF_CMDLINE_VFILES = 
+
+###############################################################################
+#                                                                             #
+# Path directives (-I, -R, -Q).                                               #
+#                                                                             #
+###############################################################################
+
+COQMF_OCAMLLIBS = -I src/utilities -I src/coq -I src/coq/termutils -I src/coq/constants -I src/coq/logicutils -I src/coq/logicutils/contexts -I src/coq/logicutils/typesandequality -I src/coq/logicutils/hofs -I src/coq/logicutils/inductive -I src/coq/logicutils/transformation -I src/coq/devutils -I src/coq/representationutils -I src/coq/decompiler -I src
+COQMF_SRC_SUBDIRS = src/utilities src/coq src/coq/termutils src/coq/constants src/coq/logicutils src/coq/logicutils/contexts src/coq/logicutils/typesandequality src/coq/logicutils/hofs src/coq/logicutils/inductive src/coq/logicutils/transformation src/coq/devutils src/coq/representationutils src/coq/decompiler src
+COQMF_COQLIBS = -I src/utilities -I src/coq -I src/coq/termutils -I src/coq/constants -I src/coq/logicutils -I src/coq/logicutils/contexts -I src/coq/logicutils/typesandequality -I src/coq/logicutils/hofs -I src/coq/logicutils/inductive -I src/coq/logicutils/transformation -I src/coq/devutils -I src/coq/representationutils -I src/coq/decompiler -I src -Q theories Plibrary -R src Plibrary
+COQMF_COQLIBS_NOML = -Q theories Plibrary -R src Plibrary
+COQMF_CMDLINE_COQLIBS =   
+
+###############################################################################
+#                                                                             #
+# Coq configuration.                                                          #
+#                                                                             #
+###############################################################################
+
+COQMF_LOCAL=0
+COQMF_COQLIB=/Users/max/.opam/default/lib/coq/
+COQMF_DOCDIR=/Users/max/.opam/default/doc/
+COQMF_OCAMLFIND=/Users/max/.opam/default/bin/ocamlfind
+COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67   -safe-string -strict-sequence
+COQMF_WARN=-warn-error +a-3
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=config lib clib kernel library engine pretyping interp gramlib gramlib/.pack parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax
+COQMF_WINDRIVE=
+
+###############################################################################
+#                                                                             #
+# Extra variables.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_OTHERFLAGS = 
+COQMF_INSTALLCOQDOCROOT = Plibrary
diff --git a/src/coq/logicutils/inductive/.indutils.ml.swp b/src/coq/logicutils/inductive/.indutils.ml.swp
new file mode 100644
index 0000000000000000000000000000000000000000..b5d06945ba3a158d55aee024be081ff6de05dfd1
GIT binary patch
literal 28672
zcmeI5e~cu@RmaCa0wIZWCb2^jDWZH9=b7{F+?^d+&Ry2l<@S7DeEyO9VH5vqdS-fN
z+c(oa>F(LPjn@fL6oe5HF^NEi*ipbqY?8>J2tpzSFen%igChZogb2d?2o@m{0)s;U
zo6mby{cCQ{Hc0p%_ekHJ>FTOiuU@_S@#?+q?d`sK?Rs-%_p%nB^INSaPi^ae@(0(?
z8h^Ldn)s(A^+i7?!z367X*x|dmiO#l-t&&jmiN5<vgOMz??!>2bi?sDjN&kDy&r<R
zMq##V7@k_r;^kl*PIgVlvr!oBN|XMse*E5Ld$~LgdwJ5XaXbq9vn(8^yTWKN>u2Fc
zpuZ%kI~l(ye@%u)0<U-p%(CI~mFKlCziiKLk;TQ^FEVd@!|_+VSQ-H|5@;mQNT88G
zBY{Q&jRYDAG!l3vNg$iPs`UXHe70-!8{PL=bKkFW*SEXx3+C>h>#lEg-_hLt?{n9A
zxv$OLKgV6a&3!*Uci&w$UyTGB2{aODB+y8pkw7DXMgoll8VNKKXe7``ppn4;K?44u
z)k<F9YW)Qe|9@`(|M#|5>+|3d@Gy7~+y_1k-Um*A_kiob3fKiM0^2|fJPW;lbaWr!
z`!28#TnPT?yjJU8a1gA5{os7?Pp@mWo(7);KLbLr0^SBL1b_S5R_k-%3h>-(TCLv%
zw}Ll-Klp)G>;2#ecqiBc-UPn)>Q?JJ;IF{f!56^;;OD@H!310ft_A0V^T3ne-)j8^
z_;rv1AG{mv00x``&IZqOsPPr>C2$|O790X^27kwa$w$F8;Asv={sue+eg`}XJ`3&#
z9|9Thz`MXzU<F(Zp5ajBG4K)av!D;QgLA=C9N2swjKEdkt>Byap-rv_#*Bl^43l``
z`AL{<niXTe+u7zc@ZzCY1XP$H+AzCq-bu%VQOg#NrjwLnN@LQUkl%}@e&Ul_<gqu&
zHICyGv#BS!Y>80G)-#4=ym6X^anv2bUAtgG_>qthEz=$ZX?7rv(#%L&r@~Sijwb$+
z38x;dfLIa`6cWfqphfk*mMU2!v!9HlC9`N4j|cY3pH9mxS~V>VlQi>&v&gu+BEmt?
z7giF2Pn5+l^0PRp)FyfNnqb3Eyoo<GJGFXGQde5-oo2NxZ~RDaIuc|VhkakfVRm-V
zFEcr@pET3XzXQK3tS!-XqqMVRxE@k?tWD^+ZgPz~9Hv<pk^vn+KIyx*e4D*6=Xd+5
zicwl5^=?+%LOy8$H3{1tev3ennD8$gZO(CSxxEJl3_{BpD$0#vWuM;crwbBATv~z6
zBb??nmL;`ID*5hi*-my$mb^I$rY0U%gqu2v%9n6y4t7V~z2@M?pgT;0bln?`<DNgZ
z`esuZDKZd1$F$d?K@#-4POF8PO23PauSLg@QO7_XAsxGM^~SwsHAZOJdYGCh2nHsL
zO*)%S<0LcFc)U4@lj(ZcH*KHdQJk5(W@z{%j$(JGb2Y?{N8!eyAnIDBlW|eWk#qf$
z*=tFEi{R?rO*83lZK$+mFC)PPS9Ppl59?^AEexx&?eRvCXqt9KDh;!m5T<sxX350t
z*pUzMbwBmecoLWwALkV8bd=dJwG%;G`XXmi=sH~x2DMXnns>$VIABP@RVrf$1@L?D
z2#Y@Bmd=PS$xPo*0!g1C2%3`x&=UU9Z5eV5I^xTi+IsO|(@t_zzkedgQoXrb{~8mS
zOHF%!lK7k5aS)BNbragm(oc~;2~zlnm}$%O5t+~|U&Xa8p|j377-rhSXg2X|?=nIw
zmD575W{mElH<T$Ek71OR?Ve2sekQF%(bj`m!e|ToU8G`eSq~y}GBDv}Iu0fQg)Bt|
za6!`!y(P&u@i%i#rL+(@B<g~c;IT(vBT>sKlV6;qX2`^c!0WU`kkaxO{Im?EOqOhV
z%ohV`p&9z)G$7r6Ziu7&BB-X<iZBc3nZlutA=D)aHiTzcwTw9#(lwqHz9no-g|tDP
zE0vl$M-}q0ySRcm3P(l1rA49x%7N4>qt2UK6!T0v<><0#`IEfGy%lr)EL)2P-HCr9
z*kjt)1<4H%)=Q>}!PFPcqq?!*3&w6?tkcmu)O}cTbY-0%Fr5wL7pqtpjTn<dTcu`o
zsb{9;GC=aEmhYyso~agP?~t;RWzws`DcEaSj*wtGoehcjr0jONyWMPUF((#DOtIO5
zwD}}yaI(Eq_Og|5LFi0;Rk^a6y?pTIJc{(|x7f;v<no-$i`%B<Dvd6LgM<-+C;Oth
zklKi&qOGPqSIy-e)y-P%9dn6yiHsa4QK_|7tf<zttJW<GidhXPv?Gi2&eei>MT|Kr
zl*;I!`Ves~U=G&%ZKsn<mMtb{ldEhJOcQfLCJUFB-z!Gf2|voZeLspL*6y+Cms#5V
zB{LHuQ%w{O5T_0MEw+fYm4S?V$t^oHsLE9722f^V-DsB6=GxGt@e)nSW(iXfvs^*j
zE(pwj2iAlB2^spno%o<hr`6}YVC?n+#R_uZV3IIBc4ujjctMhw_D$0+qBh$P#PvEL
z#cCvrzuOrEgYB|z$gCvQR@Vc&zA#;eO!h0Xj~ui4mfd37JrG}`>6I~YW+spbtIFwX
zz!`Xfjru~z=wopV+1p%Y_T+=m^-X?f<&4Xy^sZ#?i)brLTOojIN&0U_d+jD<HJ0@|
z-$E@|$ykm0rwMqIx?*<0PGG@WG-&Dd!HDTANZrMTOI?eGK@vp$z^0?0S#T=Tkn_CQ
zM&;^=8XSqE!rr)Y@0wXuxvKV;rF5L2^)M?~kcr*V(NU2U^@T|sl||U4$R>6tTTV9=
z>=KSvvd3HxLX44OkH(fl_M#?EMt&5&FIbXAzQ<B8`y$<pr5W>YM|4;0|J$&qzYWCx
z&;9R@V#D7LZUN_lf5C2l0(=hqB)Ajo0z1JEfoHMb{}6l{d=T6L_JOy63&6wJ?;i(0
z4}Ki%1s8#Tr`~^d^=}g%nolEvMgoll8VNKKXe7``ppif$ftODLMz`5w6w0A4o9z^n
zg)Mp)4*-@|;0=PIKO1MBOE=={kRxno3SpzQC27g*u6QgYg*&xlofDXea$fZRU8B%<
zbrfxTxtdm({q455Wbzi{!|=qu&qb=zkv|;0bLt?rqMoPA-&~eX!cLIZtP-oP=of1l
zR!mDd1S}4`#a`B~a#hFyyP96zU^2}%y&ko5fNXBN!`7}W7(OLi-ZTj}<j8eJ&k~Jw
zeAIH_{Rw@nNSDQWHflMrYvrI?+$v(@ZlnwHz>3_ytq{l^3o<zu9ET+8i(8Om@tJ`=
zF|gV1uC|Uto;VRDm4i~bFA80@UQSS~Xy&9c?o&qHPU81U(Q`eAQP<G|5y?%_dTC+t
zdja<u{W7-F&VMe*RdZ@CXp|iB>lj;6YgvBgO)I3UEz`3JIX_aqD-CKN!&M+k7Eh*e
z8lVI*$Go1Orn8A@TTdunfj#&q%XSxPZ#zdkch>p(Lc|;`o3)@&J+u({3#0kCp$Ya>
ztY};*Qd}HPfU0JuM!n>8MeY9|VSar?e8<@TdHnu2u=#%%oCK?&3*H3&3|s#*;6ZQ)
zxE;I)TnhdZJ73NLo&;Y4zXFC}1&DuN{QAEDj)CjIDmVb1!S4S$cocjToCF(S8N3dB
z8~^@qfrmf<t^m*D+kXx`27Vhn2tER~z}4U^@L%}yzX`qqMqmK?;O$@=cmf~(r@%wt
zwcsD{+dmE-07GyMcr|z$AO0u6$H7Uk6Z{+g`CkL;U^iF>OW-^B<{tt#fgc912VccE
ze?Rz9@C<VPEcjI*GXE)XAHaXO#;H?+AJyPJ>Z|`;4=4}B@8vv|-r<BW+Td(d=8Ywe
z#CrItZSShmEV&aq#-YcVu6R*vnbdnDUUE0Mi))6WJ?oPZ+?I);qU%=EwF0l7osvbZ
z>L%0EPUe6@VT+tlz3sq})$ZY#^WFV+yx{N0Q!^GqcI}fnxVxW2U>u_}8l|N>ZW0z<
z*91sevf{{a)far&s*O3MzTEC~hF=#2mjgU6g@SsRO#3)e<HS_cj|Q1|LR>BtsJ2b!
z1`a-*SJ=6egbQ&)u9$<-h8)V(swfJV9vvxA?VJ^Jv(LG(O$zmlnrH<bgB%hoU&kF|
z-TZbzwz7$E{Vrd^Eewf&NCl#|+|s6VcIn5ITXw~9vxm$m<uYlmZrkRrsGM*=&{SP@
z)$K@>g_F0qTwBhM-gc*`-2=19j9Ho*lnuLlTL$Hh)m0TOlC?`pd6xzp*G|caFh_C_
z8(TkD+h)v8IU=mBg?CCMthY(bsq8O!$;lL}vENH|oOpeyDc6^Rh?S*C-Yat=-`a)h
zw{1Z!-L>KL+AaH5-zua^4z^6eu}W_~6RzXJr)srif1xIJ1+6ktikbm7P1s`P^0U_}
z|DxY+DkBk`*39(}<5OKX>}HQkAC*;Wa<yjHD_f>Qw9*y?sZMbAa=F%AUq(B)+6!J8
zuqEf>6R9eV>b$a32ts#nwnw*2g>Kn;nF3%ydVAq;A>fDERvapJ3RV|VC_4{)+_W=G
zd}4lzrB)RwA5X+~kSTB0qCDz}uCq+UlOE0wV)4H7R}SQH<3}Uww=QCc)^SN(-H|=J
z$U%rmNQezwDdvf4PmqmO<c3(o0tkLM8C-&&sh<RlP^j;;1AV-?leLBD7nPATg{|HO
zzNfBKC31R^p`ZalYdVi*^MWdA=98<iuhYhssZaLw3UhNfRuOH#Nw%>8>mRW*D%C=o
zy1B7Y3V6)$V)*%Tv7H7xszTb}<A!EC#Q4&gNc3moXZ>{}>yWHHGH!JHq@w1w8`g})
ze5G0qaKK@#zzQK(*eQ_Adsvq;GRXC&=75CoP?UD-oRr@rhHAd7-gc#R9nKk)EnUu&
zbb<2Ej9XLNv8<$S#ApHO3DMdE(#5K<Ij7aE>V@{r5dr~LOZQ<n58E-~-#vZB&*y#X
zfGk#ZmNp`OwAsR&hW|K+Zql8cIL7|D*m~kUN3ZhHdCYA{_v>Ex?lPBdl5O5}UzuzR
z--8UbHeJ?qx1qd{wndXhEI&z3aW2a~YrZIpj*QiY1x>TEmloNUF5GCS;<HjSC$R6<
zy_x3Ln4|fC7`uP-4c1g;_K<bijp!{?mx#ox;AYp@mbs?stvpiZCA0zmeBMT{umkcG
zv<j73m9d7v0&{Ym*+)XUa)Y4^Q%fh}_eSW%=}6GenH$3>kRYk8TGWliIECvtBXv)v
zDv8O|wYIj7MTUv)I6B70Y@&%8)7jH5uZ8LC!OD7x1nc#AJuj=*NrJ8Qv}!$9v0ZiA
zk(6CB?oZF2S)|!b*np;&&mFR3MBs5EVUuHVkms$Cy{<ZEUF3$SmrW~TR#|N_eRUdz
zFy;timB=*NgIR&dWUO-4I@=KfgCCh#NVS@9f{vBhrc`0-FGN+6D!7uE*_J3F-sC}{
z1`-NU27E!&nU?FD)0lf4SxEjvZ1rr|1T_Y#_{7$+gh<$3HLi6@rY75q<s?tI2flo!
zu3`+8KI?r1MA$G=hTv!>acila;LAWR7x;U(y1MrnVn+G1&-D4?w8KTj8h7d-(r)*$
zDau>Yftl=?H6}=9WLZg};o(WQQNd2+8Z=u?uLylQad~C+qM2G5{4Bwgy)$2z1i0ow
z$XbCE5rxh<$V0PTSo1O_J4N^+52p^({5M?__R+Fs!Z2!tY^Ig@<UGHN;kGlDqfUA8
z|BtXg{}tO*?En1v{^zmvzW{y$yc=8!{u&$q6W}&*E4T&h0B3{eu<ySJei?iK90iwy
zOTm9&<NqEw3@!jqVAD@Q8~i1<{KvpLI06oVC2&4C2Rwrv|1I#x;0xek@JrxBzz27N
z9pGZ{_t^Ab1CN7y!AT%?|2x4I;4R?I;6m`H*!vRa{~2&6xC3;-_ptXL0k?zau=BqQ
zo&|pnz6u@#kAnNbPlFlwF>nkV1@8c_0pH*(;M3q!U=v&k-U^=OJmB}iJ>VGF4OI4s
zzxli@60pNnA6l@ZAs>3pQxW<Y0qa;fv&an1wAnlr(L5C)`;z9Vh~}w?=BWtGrRJ%K
zY9PDa>DLT4(>xWyp<DA*1e=GW_K}h1sR;KVPxDkn^HhX9TqwJ2IR<z+pNg=~2YC{}
zx)#L#{}y)m5$tlY|MU0r{UY}My&wVCg6-f>u=76%*1$IK6t?}Bfd@L^IcR(td<+c1
z&EP0d+AoV~*HqF-ppif$fkpz21R4o65@;mQNZ@}Z0h52+iH5tZUrAy$rTV*mXFjJ~
z*FUZL<-)6%lIQe#7m_0JrBRd8nzP6rOY{r@f&81VaFVCy--HI}U9N4o&wOqPSdr%^
z3eU3mTGh?VqZGs>+VFfrHZ($eZ9-JYsC?>T681cKpGnvcF`FdNqln{Hb~t3nE5HqU
z7jKks5&yh3gUmK)rV_g)iKUN2uU7I1QY}CL$RHSJzQ+p-^7j{5NB=BJ{h_{XN?xNe
z9Q&iRZJ)q5LtgmP<GnGSe=6k75A9CQWILTMLB;3&L?R~f4Id7BU4OtkJOZEi0p8AG
zV{`PGhA>(y{O@<erhT!9gv?9n)Z9~v3WdQ-xZ$E-g`#cSKtySqsL}bnKOo7UhVNQ~
zGdM+vFs^UB@f}N9_$_nmTWrK9w&d~<pyIf!Qy@#;Qp;c^fL@}JZ6f?sJA-CbULjV^
zChznj1a(@?E#U@2hDX`!H-vkoU&JBu3<r$nZ$cniY~u6UgW_!r1R=<)7o56i)Pg($
zVl-ZwQ(gG7p$}=7w~eTWeM=Je?$t0Hel6k)!HFeLM@m?(#GEZ^u0{(;zFb+gucV{o
z@e20>sU*<n^d(B?1tP+Em?jE{u$91^LC~9x_$PX!t~n;}1Jd|$4cj4>j)=M7lsvmY
WSX__yA4Ty=iRxJo2Lr+hTmJ)4Z3t`t

literal 0
HcmV?d00001

diff --git a/src/coq/logicutils/inductive/.indutils.mli.swp b/src/coq/logicutils/inductive/.indutils.mli.swp
new file mode 100644
index 0000000000000000000000000000000000000000..2e42f74aff1be856ea789f50bbd49f3de517ffe2
GIT binary patch
literal 12288
zcmeHN%ZnUE9Ii-Eqeg=f3^~M#9^74KdSX0iB2hL^SKK5RBZA6U(^I`uq`RwARlU1o
zP!EEFf<dn$c+`V<@F=2^LnQGc-uwfEc<|s|@cUIiW@g!4&uTS%bay>|kMH-W9kvID
zURqk_Pez9su04$H{DsAz9l5yUg+61MSf|l{yq3kf?Jgfb-+f~HrEfuCZ$-IYqSm`k
zcV()wUXhk7D(_hn_hNmyTfKHuHE4!<sa{cW=~QZaDj$}yQ>)TH(NL77YJ06=HZTwv
zs2JGI9zXopA$oq~;e&kd{TBl<fq}q4U?4CM7zhjm1_A?tfxy83hyhpZU~j|U+iIUL
z)b|}5?)7W91qK2Gfq}q4U?4CM7zhjm1_A?tfxtjuATaPRWIzlV`*kN{$8U%6`2T<N
z`~R=|82b|V0{9&G1h@*k3tRydFall&UIX?6yMbN6&3hTU0bB>J0v`ac0<Qos0|$UV
zcQf_}a1*!zTn9b`-UrSC%fNHM0boDy`#p@^0)7Lo1J{7Bfv<p1f%kxQAO=nY$ALv)
zAMn%N&;$GkyaQYS&H?*?2Z0~&V(eq!Bj8!!0bnn%2e`J2F%3Kf{Cp?$0LOqMzz=sY
z_C4?|kOK#STj23K;2YosK)fyj;R*}{1_A^BK?YVu%7-#eg^~UC11)}(FAXEdyH8j5
zR9XKr&^o2TQ@Jxr+NjL&HJ7o{_9aHfG^KLC(v1sg>AiYr1hg6$Uzi7YqK!yXKDPvw
z!YDVM=X2-rTnHmFJKy0^6wODpQg9>V(pYH3QzDJbW64E6<ZdK$PE!0P>0l9`Q<021
zv@a`R`{h#PP9@`w%c||daVg>vk9BUH!8dB!c)Mr!lCYB%Q!pl%Yw)%HpsiZ1ax#Ul
zq<R2SWxlG6&NDC*@w3`VOhOT@@Q$*%1;&VdUC4Zf`e!N$M;o>w$w#8m7G+S}w}p&V
zLK8H<uw_gZ>JT({3I$y8>=y>gjYBB8vf##QQ0q#Q%VETqOIO0YStqf|NS<rQZCMoB
zIIJXMQn@NqOd=c=ivo#YBff~_vawMGaf)Dj|7S%$YI&1KBngHf2C}mSm#v|8oW~;&
ztlp4AzNXyBZ=kSDOKYBM13TWr%16JxneWbsn~B|0QiqhRt8-B2-8!Wdv~SEC3pGeb
z8V1=&fOHHRt)m<iV5~AXG187m=4sF(@(o1el?JCQ>C~~Ar4a1-bRx&vl=35eolsi!
z2YNV0Md^I1z^lQgJh6|TXma0+uSDu(6T1?lGvxm!;*e85p_Og*_MOa%6h3ch03|u;
zKS_0q#Fl(*BvB;DlxAz8({ZLvF;X_8@Rt@8QZ8+4MP6ooHL_4#*N<Ekrk{yo(v=$j
zX$0wtSoo?Kwx&?ALe2ozfQw1mj>d(?92y_R?+jW}Rr-?-MQx8l;@R{sL?(}gl_ZKH
zi|=PuE>IVpHg0IdO&I!<`N{<<^vyhI2N%4^z9<SG1>Do|1}RWU^DP66asDR2c>+_?
zzA!69*raDa<tO9K28(84wWi26TSQJwue-uL7c}e*Io5E#2y0a=oPz&E(8PP&vO`-p
zI8=4UNno0YHe#RG`chf=AWS53jYDe^7>h2}>S#q#_0-na`BV7VpoWP)G{>c!j!0dQ
z&5gb@(rsBXGa=__-G#PR4N^H#j&rmktX5eC0_uE~)agm>BG+rwAW;m|w|Oq;R74AN
z0v}k%JRZsT5~b#(s-RDxq)dh`QlRsoD^a_iO6mzgtwB^nRYp>9Gk+jVj;gkaOw|q%
zFk3ZkMr$0)zG|nHl83E2Z}yb@_K4X|IXZY-xi6kOd5&iYFZq62D4br2H>VA2eNx-n
z8Q++jLma%ux?M?DQDxx5k4T)+_2FOTXf<+HWM~0?^3>|EdN|=LxE`$j20)orodqdV
peF0yWSlu9$na+1U=iSg|MbP2a;h7i@q<4#3ogvPyOp<xB?{CU(vep0q

literal 0
HcmV?d00001

diff --git a/src/coq/logicutils/transformation/.transform.ml.swp b/src/coq/logicutils/transformation/.transform.ml.swp
new file mode 100644
index 0000000000000000000000000000000000000000..ed0a65fe528bd1add017165801448f6b4ac72f58
GIT binary patch
literal 28672
zcmeI4eT-#iUB_>!E2V`(tgR?EKCCHoXFGFeUm&#G%r4uV-MVe}rQIp5pj^+~d+yBX
zo_o&SbIzTYc3DtpQlK>yjRX)u2njC@ib>^<ngW#))5a!hj7AjSqai_sqKMJz=l6S_
z^KxhI&TO|$Oz64EckVqe&vTyV_wqcyw=)Yn-+bh#xvsUl!RJ+t#-rQ!bbkG=&s=oi
zj~b1>w<>41{Hz3tANpxJNS3E}?VR3q{TrrtUpKvL&l_8j?<K7u41*{R(#BajoLLOA
znO?9uoyF6B81!cb;czjCX40fH(}_<{+r#NFSjbP!gz;j~8D>G4&SZ%frM)=mdsz@i
z<zcHIZaK>OhMEE|VhRki-t={^Xzba&Yo}1*r?<b>T=64!yod=>Prar<O@W#MH3e!4
z)D);GP*b3$z>ALp*<f4a9ZdTrZt7RM?~B%bZ*#{T_kGp6>p$d<_qp%ob=QB`9lyeT
zKeF!n#qRhg-S=bbuDiqftENCrftms}1!@Y^6sRdsQ=q0mO@W#MH3e!4)D*Y?3V7W{
z<G|&O#utF(|8xKUe_q*WJPAGt?gcAg8Qcv#a3{DK>;rqi4)AJlDfn;t`X=}b@D%tG
zkp3S6KLc(8bKp|&Bmsf1f!_pYK>+4J3;fB;xeh)IPJz3@BKQgL{mUAS{{Vju9t7_J
zcYq_{r@+PF4=-&reh2&_xCz_{t^nVDS)=h~a270r9|Ko`E5PHIG#VK=4sHc4umk+%
zOL-0$fSbW<z*XS81U9|`+Tb>@7fgd^37GsDcoIAeJ__Cq-UZ$X_JG%dtHHkzJo#tv
zRq!BqH#h)xgR8((1V_FIejEH2cssZaydGQ$E&<;sfb%%`BKQ>e82DB2E8zX$P2jsO
zsAG1RqL9Mxnr6`QTT_OziWM*EPN&0#Gz+p}=65GeC+-j8$d9tr^pd!5vL)Xv2FreA
z`f+y{`VIP;^E;uJ_{KAlzv9lDG)sn^Y{=<h)b*1}!^rFVW+lj$^qf8*4WyjI3&XWW
zb4R0L_@r@?rIY&8{x#-|X`AVN<{0DA^G17dKeJ@boQ&zYxjJQzMBT*iw8A((H5|01
z%p{1sEKZCcEt??fnpN9pvp0;)s&q;(&0B*sYxTW>9O&;}5N3YTmQ&@O+BEbt?Q7QD
z6vhi)*piN$lk`p7!@l2L@H(ej{dBPnNuwZIG|dx(RuiI_?P=yEnb|%$c|$|G*)Yhq
zpCob8Uh<+Ybu)`PUZsYaHI_C_8NE{QSe&(cF%)JFoO2&}mOkpR7lbf4i%sG$GCTM%
zNaDNwj*uIULXoN<K(jdMGP1m@aWk>k^y$Km{MN1&f_B08HbMhWnn^2dA3T2S<ouM8
zpC@iVe)BCyj?I-vjuqUjeT_Ubh<dS-PNy@USN||4k15&F-k{BdlnE4a<Sd4v<WsiD
z1LQ8g+c`P-A)ScOwg(;}*+e>~q|L;nnMJr6+zu1;j5mOAgCy`W75RB)R;8*pLPwe-
z`)G;D)&@Skr9oHJ!>Ww&(qi;eg}gV@V6pE_p>R>!mS*Wh!3Hl0vbFLMVeYmU;_g~Y
ze?<c?@%m}bh+z~g7YEHCZRdBlGrvCwnSe}B+ZPXL9!L^zt(C>?5Gg6H+x}%lqO(pL
zjWNt7%Jg~7obAPwIeiDETCF&0r%{(9A^FC+!70=VX_4`$a-kY}n`mQ}wB@Os61}pg
zvqV;-oH*{JGPd#rODQ@Z*MnYUa@9d`>!IatOV&07cG)cu+@ZG_6A%1IDCqckc2U)R
zFN>R>FDC7D;CF(a>y=KXSn}Y(l+g!PSt=r>1d&ILT|1gP%>41W<9p3PFET4WLOwlA
zk)x%+s%xAGE27K`O&IhtSs&t_Fw70G=k<dy@YDSwx>nj<#av|;%D)PUnuSEE=&Njq
zl!~0#$yJo$*zx&8d)=}J7Z7Z}*JDLVTd0a?i);~=dyFYgQs&V2f=JJ&3|{WDq%kaU
z)mv3vHf%KI<hp(@h;*xHnPVc6vVuu(qdQR9K&i2|#ST<m0Y&kgN;;X9^<AaE)%DZt
zph)HIe$OEIjKxQ%lD;`hv%S)E!m36tv0R&g%tK!kO_(9lWKJYOq>LMt#3`Nq#5rVF
z32K$z{*=e9lVy6)CytkX9qH&J&nf&WI5M+Yp>W5y+UP}@6^(K*b_7mW44-0`y8{*Q
z6GV3qhim;f86d%ZgA_+G>%nj^V1M`7YoLsL4jz(CFKr?0iEM!8>{2(`yS?B|F@o(4
zx&4eeQFPm}>Q?SWqg(QsedbWK93*kn8Vu7V=_vD8vvvwU%C+*0IT}Z?9cRak_DHd5
zXUWQGl>^dPW|-z?h)_)xd!6Dbxgeesj&f<L(6QKSMEiwIs_~*qNwBz-nH5hroUV`J
zugvIUM0r$5_rnEy|H@Jv`UbN_H>s^PRb*(LS(gu1wRBXk@=MP}pG1flXtB*<X644o
zfyj8P0XF3lOHC9TtKBSUBB@R=&LI|Kgi_?f8i*<&J+`st@qu@G=(BOhy_RjFzcKC>
z5-(Y6u~1OC+{xNrr$hNN)=<;QPOL54nYTb)GltzHs_UH=VLfAPuX8K{axNFUqgW7X
zIlCt*u@WaWOii0gBg=Ho*p}xIF4^9#T!~bTnQuiNOG8EMJ!=@Ud#D*Hwu?xSXdL^3
zTW$+YM$ouZ*&yraVNrIBlbq95-C3?;?Svmb`%lP<K1lpjwjnVjmASee*-5txt;OD)
zRas?E_m@3uO7q(hr+RjWJ4t6|9=V*RdvOcIh;n9MY(LdCw4p2N?P|nTf5(H=9-b5f
zLu<#~aqis6xV7;S_D-oSw?}Yj<VZXlous>tv0!i1{m1@1sHTej?UovQAcm0rb<`W!
zA15=6`UT8*Ygwwc_hTj*4_Ow)e{n`)nhkqB<7XXJM7_^n#e756S*83b%%`;lxtq3P
z)agDr@6^rOojKiXvAk)Dp2>zi?KbR5VVwB?2A}w0ApU=ze}5D|{)6BscoskX-@)g>
zZQvPv^M3$e2jaKC8C(vwfv51z-w9p^E(MR{hyO145V#E-0&fD>fY*R+K%ad9v5UG%
zO@W#MH3e!4)D);GP*b3$zz;SBjQs?Q5f-qE*Z1PE+YbF6?p|T<wyh0K;NO>6nV8fX
z-6f_=d^g}$96C8EH>57ytwG4*&fKlbL!Eh?)Ad}0mvQTg=!d$0oRH5*6uX)O&_MRd
zQ^8;$vAc+v5>A=zRlIr96y!{{lN*p;&X|*jZ{(snS6sFJSP^u8{twKPH0vKoW=9F6
zZfNm5n-md(YfxghMgfV2wQz4*UYAUggpW1fqEY9SAd2D@Nh6J3m}nPQbeeg(Wy_w$
zZ-m}Ohxsv#J(Fi5#DgCh6Aqq4>}<30fHq3MvZc6W`gsoXtd2(VOmbXA>d&*Ed=@#G
z^5Yj~R`_^!R(7_<Bqgq3PtCe)*OuhZCzua3KQ2g#bLt*;0lnwb&U?>~E4`2D{5i9`
z9AiNlLJphitK{v_)^^-OtXVyjuc03;k}$G)N|Jf%(JQ6t&T?MUhn3XfNy%xpY*3mt
z>oloH#Kp!GH3WZ3C^}j8WEr>d@1)uKp0X9Ih(7p8BCqK$OC*xWOV105&Z_@^7rEi^
zV)hRF|Ga+x5Age+0Fv{+21suIO7PeC|6c)*fwzM-@GO4+KY`x|%b*M9!G5p<ybSy)
zv4D?&2f)2R^7%b*HTVWGfUkjffVY6l!G95t_$%;PFa+0w7Wi9o^dATJfwzFyfoI6i
z{|4xT3GglQ@*e@$fv=N`e;;@+kR1JP@UP_DKL`3?8hnBr`z1hV@b}<R@J;X`a2PxT
zeI%cL3%C({hdla+!O!L|NsQZeOZspAE9cJb72ZhBpkbRKOsY%5L4s-H1<M8zEtegS
z3ECsBBAsoQ1zEL`!A<&Im*^fZoVLqh)RC3A6vJX&xnNBy_XxX)PD+N{65)CFS*|26
zT%Y;cM~~+-Ogj(#E9?xb`((Kt<_s1_kUh;!oXR>P)eUQtqQ5E${wf_2pq4s@d*rN@
z0k_2Xr-uY<SIs?I$I+LRtccO%y2rb+1sU9iu@yV@|I5(Ujf`56ViNgyY>h@`k=;O-
zwR6%1LXI$EJbCO{5%z}iZzGW=+$~N$g?o~J80nkTV05nb=h1wV))QKwGHb*LJL;YC
zTcY=DE*l<SDyv&mM(#MDUN$8H94R{F#_nb_UVpDlZya@`pSG7Q%Kht$dB)Vq=&dT_
z(qYLhd#b{os+yR$+9UpbO+2{4X;AeynZo?E7~;ErzU+M5>MZQvvj0k-)khWmm%J)e
zGGE1V$yZM%(zB}nfyntm%|(!S*CaL6BcpGwHM?+lMkr$2%^F+y;cS^vV?=t^%=c)^
z+-AH0!^?4GvjUt6Q>nnomw(*=ZF!8!l_a<?tg2xh74iu~(xL>y7QGCp-|{imnmac(
z;qK<qVRj_yQZ07M-(C2ZBw`l)aLQEMbe8<isj~Kh9HC2nmrtzvdW@*N07D(g%tlvB
zIW1fkK4loqqbG8!x#*xmL~UU!4RSK-sV#EUg#h_jjzzy#9#Dk2SabUYYfQ@ACHK^E
zsa-8PYn75sYO*RseZRkc61j^;2D7TpI#{@%GiK0Z*^o=E`p~w8{vGk5t>IKATMZu}
zRGFifguZ6kd7e(Sy{IKXq|zjnXs#Jwt>kDWec5Uo79SA~sj&*WR#5U0j#xKE#hWb_
zoX-Vaq6OQ{wb#0CC`H4JS9#0r4|$emG#ycG_jWcpn_c)~Ltw;Brs)J&2%;rFQ~^<t
zk-Iz;lTkvJt*O9kaT9J2oIi{;sFgla1uFF&YYe3nbTthN;b90i?ovn)G|!7<g#IIW
ze0xGW)!e*z_9uNfK2BI{*1oJ$lg2XtE#)QWgf!SxUgQQRGkMjAoYM8TiRLeeY1WWa
zw_=#JtZ~AzjG~x$Q3WPvT#Z=eBHCh$V*NahRm6pgm`qFV*Qk)vHSb<a7+K4>C@j>w
z`h!vsR6LGSxGM>7IXzZ7ir|)}?)PiRY}V4Ss;?>vlV*R@k$pD5DEx63t?ZZDl#i?|
zS<uY3Rj|C`bxPTtO6~Acydrg$-PjPdTk;cshDC$2xQG&4PLW2JvV~0xUEI~Vm_m+9
z?UBJ`wn9tU$4D5iC}eY5qQ{kb<^@V=BdP9VsSYr{6Q7V>#CT*ukh*C~3#5XFl2NU=
zVEj}zo0vr`5!Se>>3OO$;(^?Zjjm;FUKre?wFY)<uA2^xWwQOg-<9&yaLsr<^8H$o
zQFJF{DEL;Xj?=p;Mcf-|@g)C$Gk)xM@N32Y?>JxffARJI7`zAE5AFlEfXl#3!QbKc
zOI`nG!F?bGKMF1bQWx+r_#F5&cq`Zo-UxmiJdMx)B=|M(UhoTG4qOhN!S|P%f&0O`
zz&zLuE&^Y||Nk_&3)~6j!NuSaVgT<44}ut+0#}2li3NNCybt^wxD&hqyaarl*uV$C
zy&wYn!K=Y#;9JB9z5$*9Uj<U%pMeGNHZTJw!8Y(T@q;J8FM$-?30@BVlX$|n!M}mW
zzylx#C%{4Qdhk7B3ttA0fKP&tf)9X)z%PS+K>0E*zEGdLKnkEKg^hw@y?Eb#VBZo_
zJh%5Ia`R2Mychh{2{9(l_w5N8iR@qJ;~3g7Ehe1xGV2#8>K7=ifg~Pa{Q`xU>(;+k
zbM#zA=z6iVCUdu_eu1KXfkOW&GrOtyBvMw2&*LOYyn^}#3U!}~vg=A9Lj5=WBVJ?u
z0!94-#fWu^qgTH`k+tg=C|-ycC?pt5Y=RdCMXXXWpf&%09KZWxK>UB)bNze|AOH72
z2zCO=`#%7#2mi=T4}tpu|5Cj1H+g&4w*IOqP*b3$Kuv*~0yPC{3e*&+DNs|OroaVI
zzy?LO{##ekx*Dz@=qg(NLBl4c_;%_NTO&r@J<q~iy4)^BR}{wkAr&@n+wce}#O02O
ptvl5J3D9z-VYWi2DTSc6bzaSO&IA`zJKw=Pud(C>Lz4e%{2wU0imLzs

literal 0
HcmV?d00001

diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml
index 2192e59..11db6c3 100644
--- a/src/coq/logicutils/transformation/transform.ml
+++ b/src/coq/logicutils/transformation/transform.ml
@@ -103,7 +103,7 @@ let try_register_record mod_path (ind, ind') =
     ()
 
 let lookup_eliminator_error_handling ind sorts = 
-  Feedback.msg_warning (Pp.(str "start "));
+  (* Feedback.msg_warning (Pp.(str "start ")); *)
   let env = Global.env () in
   List.filter_map (fun x -> x)
   (List.map 

From d76e4be550d699b9efe58c756a424961a5114d1e Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Sun, 2 Oct 2022 23:21:53 -0500
Subject: [PATCH 37/42] Add back missing type decl

---
 src/coq/logicutils/contexts/modutils.mli | 2 +-
 src/coq/representationutils/defutils.ml  | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/coq/logicutils/contexts/modutils.mli b/src/coq/logicutils/contexts/modutils.mli
index 5e561d5..82a0219 100644
--- a/src/coq/logicutils/contexts/modutils.mli
+++ b/src/coq/logicutils/contexts/modutils.mli
@@ -38,5 +38,5 @@ val fold_module_structure_by_glob : 'a -> ('a -> Names.evaluable_global_referenc
 (*
  * Same as `fold_module_structure_by_glob` except an implicit unit accumulator.
  *)
-(* val iter_module_structure_by_glob : (evaluable_global_reference -> unit) -> module_body -> unit *)
+val iter_module_structure_by_glob : (evaluable_global_reference -> unit) -> module_body -> unit
 val fold_module_structure_by_glob : 'a -> ('a -> Globnames.global_reference -> 'a) -> 'b Declarations.generic_module_body -> 'a
diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml
index dc8a3fd..b751b74 100644
--- a/src/coq/representationutils/defutils.ml
+++ b/src/coq/representationutils/defutils.ml
@@ -13,7 +13,6 @@ open Constrextern
 
 TODO do we need to return the updated evar_map? *)
 let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh =
-  let open EConstr in
   (* XXX: "Standard" term construction combinators such as `mkApp`
      don't add any universe constraints that may be needed later for
      the kernel to check that the term is correct.

From 15132c6f89337f2458dce0213224784b436a1f10 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Sun, 2 Oct 2022 23:22:55 -0500
Subject: [PATCH 38/42] Remove vim .swp file

---
 .../logicutils/transformation/.transform.ml.swp | Bin 28672 -> 0 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)
 delete mode 100644 src/coq/logicutils/transformation/.transform.ml.swp

diff --git a/src/coq/logicutils/transformation/.transform.ml.swp b/src/coq/logicutils/transformation/.transform.ml.swp
deleted file mode 100644
index ed0a65fe528bd1add017165801448f6b4ac72f58..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 28672
zcmeI4eT-#iUB_>!E2V`(tgR?EKCCHoXFGFeUm&#G%r4uV-MVe}rQIp5pj^+~d+yBX
zo_o&SbIzTYc3DtpQlK>yjRX)u2njC@ib>^<ngW#))5a!hj7AjSqai_sqKMJz=l6S_
z^KxhI&TO|$Oz64EckVqe&vTyV_wqcyw=)Yn-+bh#xvsUl!RJ+t#-rQ!bbkG=&s=oi
zj~b1>w<>41{Hz3tANpxJNS3E}?VR3q{TrrtUpKvL&l_8j?<K7u41*{R(#BajoLLOA
znO?9uoyF6B81!cb;czjCX40fH(}_<{+r#NFSjbP!gz;j~8D>G4&SZ%frM)=mdsz@i
z<zcHIZaK>OhMEE|VhRki-t={^Xzba&Yo}1*r?<b>T=64!yod=>Prar<O@W#MH3e!4
z)D);GP*b3$z>ALp*<f4a9ZdTrZt7RM?~B%bZ*#{T_kGp6>p$d<_qp%ob=QB`9lyeT
zKeF!n#qRhg-S=bbuDiqftENCrftms}1!@Y^6sRdsQ=q0mO@W#MH3e!4)D*Y?3V7W{
z<G|&O#utF(|8xKUe_q*WJPAGt?gcAg8Qcv#a3{DK>;rqi4)AJlDfn;t`X=}b@D%tG
zkp3S6KLc(8bKp|&Bmsf1f!_pYK>+4J3;fB;xeh)IPJz3@BKQgL{mUAS{{Vju9t7_J
zcYq_{r@+PF4=-&reh2&_xCz_{t^nVDS)=h~a270r9|Ko`E5PHIG#VK=4sHc4umk+%
zOL-0$fSbW<z*XS81U9|`+Tb>@7fgd^37GsDcoIAeJ__Cq-UZ$X_JG%dtHHkzJo#tv
zRq!BqH#h)xgR8((1V_FIejEH2cssZaydGQ$E&<;sfb%%`BKQ>e82DB2E8zX$P2jsO
zsAG1RqL9Mxnr6`QTT_OziWM*EPN&0#Gz+p}=65GeC+-j8$d9tr^pd!5vL)Xv2FreA
z`f+y{`VIP;^E;uJ_{KAlzv9lDG)sn^Y{=<h)b*1}!^rFVW+lj$^qf8*4WyjI3&XWW
zb4R0L_@r@?rIY&8{x#-|X`AVN<{0DA^G17dKeJ@boQ&zYxjJQzMBT*iw8A((H5|01
z%p{1sEKZCcEt??fnpN9pvp0;)s&q;(&0B*sYxTW>9O&;}5N3YTmQ&@O+BEbt?Q7QD
z6vhi)*piN$lk`p7!@l2L@H(ej{dBPnNuwZIG|dx(RuiI_?P=yEnb|%$c|$|G*)Yhq
zpCob8Uh<+Ybu)`PUZsYaHI_C_8NE{QSe&(cF%)JFoO2&}mOkpR7lbf4i%sG$GCTM%
zNaDNwj*uIULXoN<K(jdMGP1m@aWk>k^y$Km{MN1&f_B08HbMhWnn^2dA3T2S<ouM8
zpC@iVe)BCyj?I-vjuqUjeT_Ubh<dS-PNy@USN||4k15&F-k{BdlnE4a<Sd4v<WsiD
z1LQ8g+c`P-A)ScOwg(;}*+e>~q|L;nnMJr6+zu1;j5mOAgCy`W75RB)R;8*pLPwe-
z`)G;D)&@Skr9oHJ!>Ww&(qi;eg}gV@V6pE_p>R>!mS*Wh!3Hl0vbFLMVeYmU;_g~Y
ze?<c?@%m}bh+z~g7YEHCZRdBlGrvCwnSe}B+ZPXL9!L^zt(C>?5Gg6H+x}%lqO(pL
zjWNt7%Jg~7obAPwIeiDETCF&0r%{(9A^FC+!70=VX_4`$a-kY}n`mQ}wB@Os61}pg
zvqV;-oH*{JGPd#rODQ@Z*MnYUa@9d`>!IatOV&07cG)cu+@ZG_6A%1IDCqckc2U)R
zFN>R>FDC7D;CF(a>y=KXSn}Y(l+g!PSt=r>1d&ILT|1gP%>41W<9p3PFET4WLOwlA
zk)x%+s%xAGE27K`O&IhtSs&t_Fw70G=k<dy@YDSwx>nj<#av|;%D)PUnuSEE=&Njq
zl!~0#$yJo$*zx&8d)=}J7Z7Z}*JDLVTd0a?i);~=dyFYgQs&V2f=JJ&3|{WDq%kaU
z)mv3vHf%KI<hp(@h;*xHnPVc6vVuu(qdQR9K&i2|#ST<m0Y&kgN;;X9^<AaE)%DZt
zph)HIe$OEIjKxQ%lD;`hv%S)E!m36tv0R&g%tK!kO_(9lWKJYOq>LMt#3`Nq#5rVF
z32K$z{*=e9lVy6)CytkX9qH&J&nf&WI5M+Yp>W5y+UP}@6^(K*b_7mW44-0`y8{*Q
z6GV3qhim;f86d%ZgA_+G>%nj^V1M`7YoLsL4jz(CFKr?0iEM!8>{2(`yS?B|F@o(4
zx&4eeQFPm}>Q?SWqg(QsedbWK93*kn8Vu7V=_vD8vvvwU%C+*0IT}Z?9cRak_DHd5
zXUWQGl>^dPW|-z?h)_)xd!6Dbxgeesj&f<L(6QKSMEiwIs_~*qNwBz-nH5hroUV`J
zugvIUM0r$5_rnEy|H@Jv`UbN_H>s^PRb*(LS(gu1wRBXk@=MP}pG1flXtB*<X644o
zfyj8P0XF3lOHC9TtKBSUBB@R=&LI|Kgi_?f8i*<&J+`st@qu@G=(BOhy_RjFzcKC>
z5-(Y6u~1OC+{xNrr$hNN)=<;QPOL54nYTb)GltzHs_UH=VLfAPuX8K{axNFUqgW7X
zIlCt*u@WaWOii0gBg=Ho*p}xIF4^9#T!~bTnQuiNOG8EMJ!=@Ud#D*Hwu?xSXdL^3
zTW$+YM$ouZ*&yraVNrIBlbq95-C3?;?Svmb`%lP<K1lpjwjnVjmASee*-5txt;OD)
zRas?E_m@3uO7q(hr+RjWJ4t6|9=V*RdvOcIh;n9MY(LdCw4p2N?P|nTf5(H=9-b5f
zLu<#~aqis6xV7;S_D-oSw?}Yj<VZXlous>tv0!i1{m1@1sHTej?UovQAcm0rb<`W!
zA15=6`UT8*Ygwwc_hTj*4_Ow)e{n`)nhkqB<7XXJM7_^n#e756S*83b%%`;lxtq3P
z)agDr@6^rOojKiXvAk)Dp2>zi?KbR5VVwB?2A}w0ApU=ze}5D|{)6BscoskX-@)g>
zZQvPv^M3$e2jaKC8C(vwfv51z-w9p^E(MR{hyO145V#E-0&fD>fY*R+K%ad9v5UG%
zO@W#MH3e!4)D);GP*b3$zz;SBjQs?Q5f-qE*Z1PE+YbF6?p|T<wyh0K;NO>6nV8fX
z-6f_=d^g}$96C8EH>57ytwG4*&fKlbL!Eh?)Ad}0mvQTg=!d$0oRH5*6uX)O&_MRd
zQ^8;$vAc+v5>A=zRlIr96y!{{lN*p;&X|*jZ{(snS6sFJSP^u8{twKPH0vKoW=9F6
zZfNm5n-md(YfxghMgfV2wQz4*UYAUggpW1fqEY9SAd2D@Nh6J3m}nPQbeeg(Wy_w$
zZ-m}Ohxsv#J(Fi5#DgCh6Aqq4>}<30fHq3MvZc6W`gsoXtd2(VOmbXA>d&*Ed=@#G
z^5Yj~R`_^!R(7_<Bqgq3PtCe)*OuhZCzua3KQ2g#bLt*;0lnwb&U?>~E4`2D{5i9`
z9AiNlLJphitK{v_)^^-OtXVyjuc03;k}$G)N|Jf%(JQ6t&T?MUhn3XfNy%xpY*3mt
z>oloH#Kp!GH3WZ3C^}j8WEr>d@1)uKp0X9Ih(7p8BCqK$OC*xWOV105&Z_@^7rEi^
zV)hRF|Ga+x5Age+0Fv{+21suIO7PeC|6c)*fwzM-@GO4+KY`x|%b*M9!G5p<ybSy)
zv4D?&2f)2R^7%b*HTVWGfUkjffVY6l!G95t_$%;PFa+0w7Wi9o^dATJfwzFyfoI6i
z{|4xT3GglQ@*e@$fv=N`e;;@+kR1JP@UP_DKL`3?8hnBr`z1hV@b}<R@J;X`a2PxT
zeI%cL3%C({hdla+!O!L|NsQZeOZspAE9cJb72ZhBpkbRKOsY%5L4s-H1<M8zEtegS
z3ECsBBAsoQ1zEL`!A<&Im*^fZoVLqh)RC3A6vJX&xnNBy_XxX)PD+N{65)CFS*|26
zT%Y;cM~~+-Ogj(#E9?xb`((Kt<_s1_kUh;!oXR>P)eUQtqQ5E${wf_2pq4s@d*rN@
z0k_2Xr-uY<SIs?I$I+LRtccO%y2rb+1sU9iu@yV@|I5(Ujf`56ViNgyY>h@`k=;O-
zwR6%1LXI$EJbCO{5%z}iZzGW=+$~N$g?o~J80nkTV05nb=h1wV))QKwGHb*LJL;YC
zTcY=DE*l<SDyv&mM(#MDUN$8H94R{F#_nb_UVpDlZya@`pSG7Q%Kht$dB)Vq=&dT_
z(qYLhd#b{os+yR$+9UpbO+2{4X;AeynZo?E7~;ErzU+M5>MZQvvj0k-)khWmm%J)e
zGGE1V$yZM%(zB}nfyntm%|(!S*CaL6BcpGwHM?+lMkr$2%^F+y;cS^vV?=t^%=c)^
z+-AH0!^?4GvjUt6Q>nnomw(*=ZF!8!l_a<?tg2xh74iu~(xL>y7QGCp-|{imnmac(
z;qK<qVRj_yQZ07M-(C2ZBw`l)aLQEMbe8<isj~Kh9HC2nmrtzvdW@*N07D(g%tlvB
zIW1fkK4loqqbG8!x#*xmL~UU!4RSK-sV#EUg#h_jjzzy#9#Dk2SabUYYfQ@ACHK^E
zsa-8PYn75sYO*RseZRkc61j^;2D7TpI#{@%GiK0Z*^o=E`p~w8{vGk5t>IKATMZu}
zRGFifguZ6kd7e(Sy{IKXq|zjnXs#Jwt>kDWec5Uo79SA~sj&*WR#5U0j#xKE#hWb_
zoX-Vaq6OQ{wb#0CC`H4JS9#0r4|$emG#ycG_jWcpn_c)~Ltw;Brs)J&2%;rFQ~^<t
zk-Iz;lTkvJt*O9kaT9J2oIi{;sFgla1uFF&YYe3nbTthN;b90i?ovn)G|!7<g#IIW
ze0xGW)!e*z_9uNfK2BI{*1oJ$lg2XtE#)QWgf!SxUgQQRGkMjAoYM8TiRLeeY1WWa
zw_=#JtZ~AzjG~x$Q3WPvT#Z=eBHCh$V*NahRm6pgm`qFV*Qk)vHSb<a7+K4>C@j>w
z`h!vsR6LGSxGM>7IXzZ7ir|)}?)PiRY}V4Ss;?>vlV*R@k$pD5DEx63t?ZZDl#i?|
zS<uY3Rj|C`bxPTtO6~Acydrg$-PjPdTk;cshDC$2xQG&4PLW2JvV~0xUEI~Vm_m+9
z?UBJ`wn9tU$4D5iC}eY5qQ{kb<^@V=BdP9VsSYr{6Q7V>#CT*ukh*C~3#5XFl2NU=
zVEj}zo0vr`5!Se>>3OO$;(^?Zjjm;FUKre?wFY)<uA2^xWwQOg-<9&yaLsr<^8H$o
zQFJF{DEL;Xj?=p;Mcf-|@g)C$Gk)xM@N32Y?>JxffARJI7`zAE5AFlEfXl#3!QbKc
zOI`nG!F?bGKMF1bQWx+r_#F5&cq`Zo-UxmiJdMx)B=|M(UhoTG4qOhN!S|P%f&0O`
zz&zLuE&^Y||Nk_&3)~6j!NuSaVgT<44}ut+0#}2li3NNCybt^wxD&hqyaarl*uV$C
zy&wYn!K=Y#;9JB9z5$*9Uj<U%pMeGNHZTJw!8Y(T@q;J8FM$-?30@BVlX$|n!M}mW
zzylx#C%{4Qdhk7B3ttA0fKP&tf)9X)z%PS+K>0E*zEGdLKnkEKg^hw@y?Eb#VBZo_
zJh%5Ia`R2Mychh{2{9(l_w5N8iR@qJ;~3g7Ehe1xGV2#8>K7=ifg~Pa{Q`xU>(;+k
zbM#zA=z6iVCUdu_eu1KXfkOW&GrOtyBvMw2&*LOYyn^}#3U!}~vg=A9Lj5=WBVJ?u
z0!94-#fWu^qgTH`k+tg=C|-ycC?pt5Y=RdCMXXXWpf&%09KZWxK>UB)bNze|AOH72
z2zCO=`#%7#2mi=T4}tpu|5Cj1H+g&4w*IOqP*b3$Kuv*~0yPC{3e*&+DNs|OroaVI
zzy?LO{##ekx*Dz@=qg(NLBl4c_;%_NTO&r@J<q~iy4)^BR}{wkAr&@n+wce}#O02O
ptvl5J3D9z-VYWi2DTSc6bzaSO&IA`zJKw=Pud(C>Lz4e%{2wU0imLzs


From eafd2c4625f252f10b5291ab28a88438160da9d0 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Sun, 2 Oct 2022 23:27:57 -0500
Subject: [PATCH 39/42] Silence more build warnings

---
 Makefile.local | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.local b/Makefile.local
index e1a43fb..b5dfc1e 100644
--- a/Makefile.local
+++ b/Makefile.local
@@ -1 +1 @@
-OCAMLWARN=-warn-error +a-3-8-40-32-28
+OCAMLWARN=-warn-error +a-3-8-40-32-28-33

From 3630afd684cbb10270b317d7ca24889d3f36c19b Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Sun, 2 Oct 2022 23:35:00 -0500
Subject: [PATCH 40/42] Change types of api func

---
 src/coq/logicutils/contexts/modutils.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq/logicutils/contexts/modutils.mli b/src/coq/logicutils/contexts/modutils.mli
index 82a0219..b23e60e 100644
--- a/src/coq/logicutils/contexts/modutils.mli
+++ b/src/coq/logicutils/contexts/modutils.mli
@@ -38,5 +38,5 @@ val fold_module_structure_by_glob : 'a -> ('a -> Names.evaluable_global_referenc
 (*
  * Same as `fold_module_structure_by_glob` except an implicit unit accumulator.
  *)
-val iter_module_structure_by_glob : (evaluable_global_reference -> unit) -> module_body -> unit
+val iter_module_structure_by_glob : (Globnames.global_reference -> unit) -> 'a Declarations.generic_module_body -> unit
 val fold_module_structure_by_glob : 'a -> ('a -> Globnames.global_reference -> 'a) -> 'b Declarations.generic_module_body -> 'a

From a4a353d2b8db45124a3b6f2bf2b404b4ba9514f1 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Sun, 2 Oct 2022 23:45:56 -0500
Subject: [PATCH 41/42] Fix forward ref issue

---
 src/coq/logicutils/contexts/envutils.ml | 5 +++--
 src/coq/representationutils/defutils.ml | 1 +
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/coq/logicutils/contexts/envutils.ml b/src/coq/logicutils/contexts/envutils.ml
index 22593b7..41c8e6f 100644
--- a/src/coq/logicutils/contexts/envutils.ml
+++ b/src/coq/logicutils/contexts/envutils.ml
@@ -6,12 +6,13 @@ open Utilities
 open Environ
 open Constr
 open Declarations
-open Contextutils
 open Evd
 open Names
 open Nameutils
 open Stateutils
-   
+
+open Contextutils
+
 (* Look up all indexes from is in env *)
 let lookup_rels (is : int list) (env : env) : rel_declaration list =
  List.map (fun i -> lookup_rel i env) is
diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml
index b751b74..dc8a3fd 100644
--- a/src/coq/representationutils/defutils.ml
+++ b/src/coq/representationutils/defutils.ml
@@ -13,6 +13,7 @@ open Constrextern
 
 TODO do we need to return the updated evar_map? *)
 let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh =
+  let open EConstr in
   (* XXX: "Standard" term construction combinators such as `mkApp`
      don't add any universe constraints that may be needed later for
      the kernel to check that the term is correct.

From c8cdf42d7dbb08c76dcfa05ed9521f6c2a7a6c35 Mon Sep 17 00:00:00 2001
From: Max Fan <git@max.fan>
Date: Thu, 3 Nov 2022 15:07:21 -0500
Subject: [PATCH 42/42] Set allow_evars to true (bug fix)

---
 src/coq/representationutils/defutils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml
index dc8a3fd..f19548a 100644
--- a/src/coq/representationutils/defutils.ml
+++ b/src/coq/representationutils/defutils.ml
@@ -43,7 +43,7 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh =
       sigma
   in
   let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *)
-  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:tyopt ~body in
+  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:true ~opaque ~poly sigma udecl ~types:tyopt ~body in
   let ubinders = Evd.universe_binders sigma in
   let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
   let kind = Decls.(IsDefinition Definition) in