Ported plugin to Coq 8.13

.gitignore

@@ -23,3 +23,8 @@ plugin/Makefile
 plugin/.merlin
 *.out
 _opam
+_build
+/Makefile
+/Makefile.conf
+.merlin
+/src/plibrary.ml

dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.6)
+(using coq 0.6)
+(name my-plugin)

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 (KerName.make coq_init_logic (Label.make "eq")), 0)
 
 (* Constructor for quality *)
 let eq_refl : types =
@@ -70,8 +70,9 @@ let apply_eq (app : eq_app) : types =
  * Deconstruct an eq type
  *)
 let dest_eq (trm : types) : eq_app =
-  let [at_type; trm1; trm2] = unfold_args trm in
-  { at_type; trm1; trm2 }
+  match unfold_args trm with
+  | [at_type; trm1; trm2] -> { at_type; trm1; trm2 }
+  | _ -> assert false
 
 (*
  * An application of eq_sym
@@ -93,10 +94,12 @@ let apply_eq_sym (app : eq_sym_app) : types =
  * Deconstruct an eq type
  *)
 let dest_eq_sym (trm : types) : eq_sym_app =
-  let [at_type; trm1; trm2; eq_proof] = unfold_args trm in
-  let eq_typ = { at_type; trm1; trm2 } in
-  { eq_typ; eq_proof }
-
+  match unfold_args trm with
+  | [at_type; trm1; trm2; eq_proof] ->
+    let eq_typ = { at_type; trm1; trm2 } in
+    { eq_typ; eq_proof }
+  | _ -> assert false
+
 (*
  * An application of eq_ind
  *)
@@ -120,8 +123,10 @@ let apply_eq_ind (app : eq_ind_app) : types =
  * Deconstruct an eq_ind
  *)
 let dest_eq_ind (trm : types) : eq_ind_app =
-  let [at_type; trm1; p; b; trm2; h] = unfold_args trm in
-  { at_type; trm1; p; b; trm2; h }
+  match unfold_args trm with
+  | [at_type; trm1; p; b; trm2; h] ->
+    { at_type; trm1; p; b; trm2; h }
+  | _ -> assert false
 
 (*
  * An application of eq_refl
@@ -142,8 +147,10 @@ let apply_eq_refl (app : eq_refl_app) : types =
  * Deconstruct an eq_refl
  *)
 let dest_eq_refl (trm : types) : eq_refl_app =
-  let [typ; trm] = unfold_args trm in
-  { typ; trm }
+  match unfold_args trm with
+  | [typ; trm] ->
+    { typ; trm }
+  | _ -> assert false
 
 (*
  * Deconstruct an eq_refl.

src/coq/constants/idutils.ml

@@ -4,7 +4,6 @@
 
 open Constr
 open Names
-open Environ
 open Evd
 
 let coq_init_datatypes =
@@ -27,7 +26,7 @@ let id_typ : types =
 let identity_term env sigma typ : evar_map * types =
   let sigma, sort_family = Inference.infer_sort env sigma typ in
   match sort_family with
-  | InProp ->
+  | Sorts.InProp ->
      (sigma, mkApp (id_prop, Array.make 1 typ))
   | _ ->
      (sigma, mkApp (id_typ, Array.make 1 typ))

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 (KerName.make coq_init_data (Label.make "prod")), 0)
 
 (* Introduction for sigma types *)
 let pair : constr =
@@ -55,9 +55,11 @@ let apply_pair (app : pair_app) =
  * Deconsruct a sigT type from a type
  *)
 let dest_pair (trm : constr) =
-  let [typ1; typ2; trm1; trm2] = unfold_args trm in
-  { typ1; typ2; trm1; trm2 }
-
+  match unfold_args trm with
+  | [typ1; typ2; trm1; trm2] ->
+    { typ1; typ2; trm1; trm2 }
+  | _ -> assert false
+
 (*
  * An application of prod
  *)
@@ -77,8 +79,10 @@ let apply_prod (app : prod_app) : types =
  * Deconstruct a prod
  *)
 let dest_prod (trm : types) : prod_app =
-  let [typ1; typ2] = unfold_args trm in
-  { typ1; typ2 }
+  match unfold_args trm with
+  | [typ1; typ2] ->
+    { typ1; typ2 }
+  | _ -> assert false
 
 (*
  * An application of prod_rect
@@ -106,9 +110,11 @@ let elim_prod (app : prod_elim) =
  * Deconstruct an application of prod
  *)
 let dest_prod_elim (trm : constr) =
-  let [typ1; typ2; p; proof; arg] = unfold_args trm in
-  let to_elim = { typ1; typ2 } in
-  { to_elim; p; proof; arg }
+  match unfold_args trm with
+  | [typ1; typ2; p; proof; arg] ->
+    let to_elim = { typ1; typ2 } in
+    { to_elim; p; proof; arg }
+  | _ -> assert false
 
 (*
  * First projection of a prod

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 (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 (KerName.make coq_init_logic (Label.make "and")), 0)
 
 (* constructor of /\ *)
 let conj : types =

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 (KerName.make coq_init_specif (Label.make "sigT")), 0)
 
 (* Introduction for sigma types *)
 let existT : types =
@@ -55,8 +55,10 @@ let pack_existT (app : existT_app) : types =
  * Deconstruct an existT term
  *)
 let dest_existT (trm : types) : existT_app =
-  let [index_type; packer; index; unpacked] = unfold_args trm in
-  { index_type; packer; index; unpacked }
+  match unfold_args trm with
+  | [index_type; packer; index; unpacked] ->
+    { index_type; packer; index; unpacked }
+  | _ -> assert false
 
 (*
  * An application of sigT
@@ -77,8 +79,10 @@ let pack_sigT (app : sigT_app) =
  * Deconsruct a sigT type from a type
  *)
 let dest_sigT (typ : types) =
-  let [index_type; packer] = unfold_args typ in
-  { index_type; packer }
+  match unfold_args typ with
+  | [index_type; packer] ->
+    { index_type; packer }
+  | _ -> assert false
 
 (*
  * Build the eta-expansion of a term known to have a sigma type.
@@ -116,9 +120,11 @@ let elim_sigT (app : sigT_elim) =
  * Deconstruct an application of sigT_rect
  *)
 let dest_sigT_elim (trm : types) =
-  let [index_type; packer; packed_type; unpacked; arg] = unfold_args trm in
-  let to_elim = { index_type ; packer } in
-  { to_elim; packed_type; unpacked; arg }
+  match unfold_args trm with
+  | [index_type; packer; packed_type; unpacked; arg] ->
+    let to_elim = { index_type ; packer } in
+    { to_elim; packed_type; unpacked; arg }
+  | _ -> assert false
 
 (*
  * Left projection of a sigma type