lthms · lthms · May 16, 2022
diff --git a/coq-freespec-core.opam b/coq-freespec-core.opam
@@ -25,7 +25,7 @@ build: [
 depends: [
   "ocaml"
   "dune" {>= "2.5"}
-  "coq" {>= "8.12" & < "8.14~" | = "dev"}
+  "coq" {>= "8.12" & < "8.16~" | = "dev"}
   "coq-ext-lib" {>= "0.11.2" | = "dev"}
 ]
 

diff --git a/coq-freespec-exec.opam b/coq-freespec-exec.opam
@@ -24,7 +24,7 @@ build: [
 depends: [
   "ocaml"
   "dune" {>= "2.5"}
-  "coq" {>= "8.12" & < "8.14~" | = "dev"}
+  "coq" {>= "8.12" & < "8.15~" | = "dev"}
   "coq-freespec-core" {= "dev"}
   "coq-freespec-ffi" {= "dev"}
 ]

diff --git a/coq-freespec-ffi.opam b/coq-freespec-ffi.opam
@@ -23,7 +23,7 @@ build: [
 depends: [
   "ocaml"
   "dune" {>= "2.5"}
-  "coq" {>= "8.12" & < "8.14~" | = "dev"}
+  "coq" {>= "8.12" & < "8.15~" | = "dev"}
   "coq-freespec-core" {= "dev"}
   "coq-coqffi" {= "dev" | >= "1.0~"}
   "coq-simple-io" {>= "1.0" & < "2.0" | = "dev"}

diff --git a/theories/Core/Contract.v b/theories/Core/Contract.v
@@ -149,7 +149,7 @@ Lemma contract_equ_sym `(c1 : contract i Ω1) `(c2 : contract i Ω2)
 
 Proof.
   induction equ.
-  apply mk_contract_equ with (f0:=g) (g0:=f).
+  apply (mk_contract_equ c2 c1 g f).
   + apply iso2.
   + apply iso1.
   + intros ω α p.

diff --git a/theories/Core/Impure.v b/theories/Core/Impure.v
@@ -59,6 +59,7 @@ Fixpoint impure_bind {i α β} (p : impure i α) (f : α -> impure i β) : impur
 Definition impure_map {i α β} (f : α -> β) (p : impure i α) : impure i β :=
   impure_bind p (fun x => local (f x)).
 
+#[export]
 Instance impure_Functor i : Functor (impure i) :=
   { fmap := @impure_map i
   }.
@@ -68,11 +69,13 @@ Definition impure_pure {i α} (x : α) : impure i α := local x.
 Definition impure_apply {i α β} (p : impure i (α -> β)) (q : impure i α) : impure i β :=
   impure_bind p (fun f => fmap f q).
 
+#[export]
 Instance impure_Applicative i : Applicative (impure i) :=
   { pure := @impure_pure i
   ; ap := @impure_apply i
   }.
 
+#[export]
 Instance impure_Monad (i : interface) : Monad (impure i) :=
   { ret := @impure_pure i
   ; bind := @impure_bind i
@@ -108,6 +111,7 @@ Definition request `{Provide ix i} {α} (e : i α) : impure ix α :=
     Haskell) to write monadic functions more easily.  These notations live
     inside the [monad_scope]. *)
 
+#[export]
 Instance store_monad_state (s : Type) (ix : interface) `{Provide ix (STORE s)}
   : MonadState s (impure ix) :=
   { put := fun (x : s) => request (Put x)

diff --git a/theories/Core/ImpureFacts.v b/theories/Core/ImpureFacts.v
@@ -41,7 +41,7 @@ Infix "===" := impure_eq : impure_scope.
     of the treatment of the continuation. There is no much effort to put into
     proving this is indeed a proper equivalence. *)
 
-#[program]
+#[program, export]
 Instance impure_Equivalence i α : @Equivalence (impure i α) impure_eq := {}.
 
 Next Obligation.
@@ -89,7 +89,7 @@ Ltac change_impure_bind :=
     assert (R: function_eq impure_eq f g); [ intros ?x | now rewrite R ]
   end.
 
-#[program]
+#[program, export]
 Instance request_then_Proper i α β
   : Proper (eq ==> function_eq impure_eq ==> impure_eq) (@request_then i α β).
 
@@ -102,7 +102,7 @@ Next Obligation.
   now rewrite equ.
 Qed.
 
-#[program]
+#[program, export]
 Instance impure_bind_Proper i α β
   : Proper (impure_eq ==> function_eq impure_eq ==> impure_eq) (@impure_bind i α β).
 
@@ -118,6 +118,7 @@ Next Obligation.
     apply H.
 Qed.
 
+#[export]
 Instance impure_map_Proper i α β
   : Proper (function_eq eq ==> impure_eq ==> impure_eq) (@impure_map i α β).
 
@@ -130,7 +131,7 @@ Proof.
   now rewrite equf.
 Qed.
 
-#[program]
+#[program, export]
 Instance impure_apply_Proper i α β
   : Proper (impure_eq ==> impure_eq ==> impure_eq) (@impure_apply i α β).
 

diff --git a/theories/Core/Init.v b/theories/Core/Init.v
@@ -37,7 +37,7 @@ Notation "m '~>' n" :=
 Definition function_eq {a b} (r : b -> b -> Prop) (f g : a -> b) : Prop :=
   forall (x : a), r (f x) (g x).
 
-#[program]
+#[program, export]
 Instance function_eq_Equivalence a `(Equivalence b r)
   : @Equivalence (a -> b) (function_eq r).
 

diff --git a/theories/Core/Interface.v b/theories/Core/Interface.v
@@ -86,6 +86,7 @@ Class Provide (ix i : interface) `{MayProvide ix i} : Type :=
     ridiculously high priority number to ensure it is selected only if no other
     instances are found. *)
 
+#[export]
 Instance default_MayProvide (i j : interface) : MayProvide i j|1000 :=
   { proj_p := fun _ _ => None
   }.
@@ -140,15 +141,17 @@ with_state true (with_state false get)
 
     will return false (that is, the variable in the inner store). *)
 
+#[export]
 Instance refl_MayProvide (i : interface) : MayProvide i i :=
   { proj_p := fun _ e => Some e
   }.
 
-#[program]
+#[program, export]
 Instance refl_Provide (i : interface) : @Provide i i (refl_MayProvide i) :=
   { inj_p := fun (a : Type) (e : i a) => e
   }.
 
+#[export]
 Instance iplus_left_MayProvide (ix i j : interface) `{MayProvide ix i}
   : MayProvide (ix + j) i :=
   { proj_p := fun _ e =>
@@ -158,7 +161,7 @@ Instance iplus_left_MayProvide (ix i j : interface) `{MayProvide ix i}
                 end
   }.
 
-#[program]
+#[program, export]
 Instance iplus_left_Provide (ix i j : interface) `{Provide ix i}
   : @Provide (ix + j) i (iplus_left_MayProvide ix i j) :=
   { inj_p := fun (a : Type) (e : i a) => in_left (inj_p e)
@@ -168,6 +171,7 @@ Next Obligation.
   now rewrite proj_inj_p_equ.
 Qed.
 
+#[export]
 Instance iplus_right_MayProvide (i jx j : interface) `{MayProvide jx j}
   : MayProvide (i + jx) j :=
   { proj_p := fun _ e =>
@@ -177,7 +181,7 @@ Instance iplus_right_MayProvide (i jx j : interface) `{MayProvide jx j}
                 end
   }.
 
-#[program]
+#[program, export]
 Instance iplus_right_Provide (i jx j : interface) `{Provide jx j}
   : @Provide (i + jx) j (iplus_right_MayProvide i jx j) :=
   { inj_p := fun _ e => in_right (inj_p e)
@@ -205,43 +209,43 @@ Ltac find_may_provide :=
 
 #[global] Hint Extern 1 (MayProvide (iplus _ _) _) => find_may_provide : typeclass_instances.
 
-#[program]
+#[program, export]
 Instance refl_Distinguish (i j : interface)
   : @Distinguish i i j  (@refl_MayProvide i) (@refl_Provide i) (@default_MayProvide i j).
 
-#[program]
+#[program, export]
 Instance iplus_left_default_Distinguish (ix jx i j : interface)
    `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1}
   : @Distinguish (ix + jx) i j
                  (@iplus_left_MayProvide ix i jx M1)
                  (@iplus_left_Provide ix i jx M1 P1)
                  (@default_MayProvide _ j).
 
-#[program]
+#[program, export]
 Instance iplus_right_default_Distinguish (ix jx i j : interface)
    `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1}
   : @Distinguish (ix + jx) i j
                  (@iplus_right_MayProvide ix jx i M1)
                  (@iplus_right_Provide ix jx i M1 P1)
                  (@default_MayProvide _ j).
 
-#[program]
+#[program, export]
 Instance iplus_left_may_right_Distinguish (ix jx i j : interface)
    `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1} `{M2 : MayProvide jx j}
   : @Distinguish (ix + jx) i j
                  (@iplus_left_MayProvide ix i jx M1)
                  (@iplus_left_Provide ix i jx M1 P1)
                  (@iplus_right_MayProvide ix jx j M2).
 
-#[program]
+#[program, export]
 Instance iplus_right_may_left_Distinguish (ix jx i j : interface)
    `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1} `{M2 : MayProvide ix j}
   : @Distinguish (ix + jx) i j
                  (@iplus_right_MayProvide ix jx i M1)
                  (@iplus_right_Provide ix jx i M1 P1)
                  (@iplus_left_MayProvide ix j jx M2).
 
-#[program]
+#[program, export]
 Instance iplus_left_distinguish_left_Distinguish (ix jx i j : interface)
    `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1} `{M2 : MayProvide ix j}
    `{@Distinguish ix i j M1 P1 M2}
@@ -254,7 +258,7 @@ Next Obligation.
   apply distinguish.
 Defined.
 
-#[program]
+#[program, export]
 Instance iplus_right_distinguish_right_Distinguish (ix jx i j : interface)
    `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1} `{M2 : MayProvide jx j}
    `{@Distinguish jx i j M1 P1 M2}