Add coq-of-ocaml 2.5.3+4.14 with modern typeclass visibility

released/packages/coq-of-ocaml/coq-of-ocaml.2.5.3+4.14/files/global-instances.patch

@@ -0,0 +1,83 @@
+diff --git a/proofs/Basics.v b/proofs/Basics.v
+index 475ac7a3..8cdef65f 100644
+--- a/proofs/Basics.v
++++ b/proofs/Basics.v
+@@ -122,7 +122,7 @@ Definition try_with {A : Set} (e : unit -> A) (_with : extensible_type -> A)
+ Module Unit.
+   Definition lt (x y : unit) : Prop := False.
+
+-  Instance strict_order : StrictOrder lt.
++  Global Instance strict_order : StrictOrder lt.
+     refine {|
+       StrictOrder_Irreflexive := _;
+       StrictOrder_Transitive := _ |}.
+@@ -133,7 +133,7 @@ Module Unit.
+       exact Rxy.
+   Qed.
+
+-  Instance order_dec : OrderDec strict_order.
++  Global Instance order_dec : OrderDec strict_order.
+     refine {|
+       compare := fun x y => Eq;
+       compare_is_sound := fun x y => CompEq _ _ _ |}.
+@@ -145,7 +145,7 @@ Module Bool.
+   Inductive lt : bool -> bool -> Prop :=
+   | lt_intro : lt false true.
+
+-  Instance strict_order : StrictOrder lt.
++  Global Instance strict_order : StrictOrder lt.
+     refine {|
+       StrictOrder_Irreflexive := _;
+       StrictOrder_Transitive := _ |}.
+@@ -156,7 +156,7 @@ Module Bool.
+       constructor.
+   Qed.
+
+-  Instance order_dec : OrderDec strict_order.
++  Global Instance order_dec : OrderDec strict_order.
+     refine {|
+       compare := fun x y =>
+         match (x, y) with
+@@ -172,9 +172,9 @@ Module Bool.
+ End Bool.
+
+ Module Z.
+-  Instance eq_dec : EqDec (eq_setoid Z) := Z.eq_dec.
++  Global Instance eq_dec : EqDec (eq_setoid Z) := Z.eq_dec.
+
+-  Instance order_dec : OrderDec Z.lt_strorder := {|
++  Global Instance order_dec : OrderDec Z.lt_strorder := {|
+     compare := Z.compare;
+     compare_is_sound := Z.compare_spec |}.
+ End Z.
+@@ -307,13 +307,13 @@ Module Char.
+     Qed.
+   End Lt.
+
+-  Instance strict_order : StrictOrder Lt.t :=
++  Global Instance strict_order : StrictOrder Lt.t :=
+     {|
+       StrictOrder_Irreflexive := Lt.irreflexivity;
+       StrictOrder_Transitive := Lt.transitivity;
+     |}.
+
+-  Instance order_dec : OrderDec strict_order.
++  Global Instance order_dec : OrderDec strict_order.
+     refine {|
+       compare := fun c1 c2 => (N_of_ascii c1 ?= N_of_ascii c2) % N;
+       compare_is_sound := fun c1 c2 => _;
+@@ -480,12 +480,12 @@ Module String.
+       now rewrite (proj2 (N.ltb_lt _ _) H_gt_c1c2).
+   Qed.
+
+-  Instance strict_order : StrictOrder Lt.t := {|
++  Global Instance strict_order : StrictOrder Lt.t := {|
+       StrictOrder_Irreflexive := Lt.irreflexivity;
+       StrictOrder_Transitive := Lt.transitivity;
+     |}.
+
+-  Instance order_dec : OrderDec strict_order.
++  Global Instance order_dec : OrderDec strict_order.
+     refine {|
+       compare := fun s1 s2 =>
+         if String.eqb s1 s2 then

released/packages/coq-of-ocaml/coq-of-ocaml.2.5.3+4.14/opam

@@ -0,0 +1,49 @@
+opam-version: "2.0"
+maintainer: "dev@clarus.me"
+homepage: "https://github.com/formal-land/coq-of-ocaml"
+dev-repo: "git+https://github.com/formal-land/coq-of-ocaml.git"
+bug-reports: "https://github.com/formal-land/coq-of-ocaml/issues"
+authors: ["Guillaume Claret"]
+license: "MIT"
+build: [
+  ["sh" "-c" "cd proofs && ./configure.sh"] {coq:installed}
+  [make "-C" "proofs" "-j%{jobs}%"] {coq:installed}
+  ["dune" "build" "-p" name "-j" jobs]
+]
+install: [
+  [make "-C" "proofs" "install"] {coq:installed}
+]
+depends: [
+  "angstrom" {>= "0.15.0"}
+  "csexp" {>= "1.5.0"}
+  "dune" {>= "2.9"}
+  "ocaml" {>= "4.14" & < "4.15"}
+  "ocamlfind" {>= "1.5.2"}
+  "result"
+  "smart-print"
+  "yojson" {>= "1.6.0"}
+]
+depopts: [
+  "coq"
+]
+patches: [
+  "global-instances.patch"
+]
+extra-files: [
+  "global-instances.patch"
+  "sha256=0c83b6821636dca049a726a716fbfa59b1911a3e0de9cf2a81b79257cc63ef67"
+]
+tags: [
+  "keyword:compilation"
+  "keyword:OCaml"
+  "logpath:CoqOfOCaml"
+]
+synopsis: "Compile a subset of OCaml to Coq"
+
+url {
+  src: "https://github.com/formal-land/coq-of-ocaml/releases/download/2.5.3/coq-of-ocaml-full.2.5.3+4.14.tar.gz"
+  checksum: [
+    "sha256=1c6d414ae8e4babfd79f82cb667cdaaf11b4c3b76dc83de4c23f6ee8ec6affff"
+    "sha512=4b017b5892ef0c665a5ff5da292ec5cbdd1a103dfb7193553b78d25693787acd359a30028c335b300883d555786d3787258fe7a57d63cd53b94edc6b40e8ffbe"
+  ]
+}