From 48c890c049d67db4e23936035d22b3fb07aa0770 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 8 Aug 2024 16:49:24 +0900
Subject: [PATCH] fix wochoice/ring

---
 classical/wochoice.v            | 4 ++--
 theories/lang_syntax.v          | 4 ++--
 theories/lang_syntax_examples.v | 6 ++++--
 theories/prob_lang.v            | 2 +-
 4 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/classical/wochoice.v b/classical/wochoice.v
index d291241465..43f5593ad0 100644
--- a/classical/wochoice.v
+++ b/classical/wochoice.v
@@ -259,7 +259,7 @@ move=> Rxx Rtr Cch sCS.
 pose CSch X := `[< [/\ chain R X, {subset C <= X} & {subset X <= S}] >].
 pose Rch (X Y : {pred T}) := `[< {subset X <= Y} >].
 have: {in CSch & &, transitive Rch}.
-  by apply: in3W => X Y Z /asboolP-sXY /asboolP-sYZ; apply/asboolP=> x /sXY/sYZ.
+  by move=> X Y Z ? ? ? /asboolP-sXY /asboolP-sYZ; apply/asboolP => x /sXY/sYZ.
 have /Zorn's_lemma/[apply]: {in CSch, reflexive Rch} by move=> X _; apply/asboolP.
 case=> [XX CSchXX XXwo | M /asboolP[Mch sCM sMS] maxM]; last first.
   exists M; split=> // X Xch sMX sXS.
@@ -301,7 +301,7 @@ have initRtr: transitive initR.
   move=> R2 R1 R3 /asboolP[D12 R12] /asboolP[D23 R23]; apply/asboolP.
   split=> [x /D12/D23// | x y D1x D3y]; rewrite R23 ?(D12 x) //.
   by case D2y: (y \in R2.1); [apply: R12 | rewrite (contraFF (D12 y))].
-have: {in pwo & &, transitive initR} by apply: in3W.
+have: {in pwo & &, transitive initR} by move=> X Y Z ? ? ?; exact: initRtr.
 have/Zorn's_lemma/[apply]: {in pwo, reflexive initR} by [].
 case=> [C pwoC Cch | [D R] /asboolP/=pwoR maxR].
   have /(@wo_chainW ({pred T} * rel T)%type) {}Cch := Cch.
diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v
index 1e011f3de5..691735dcba 100644
--- a/theories/lang_syntax.v
+++ b/theories/lang_syntax.v
@@ -6,7 +6,7 @@ From mathcomp Require Import functions cardinality fsbigop.
 Require Import signed reals ereal topology normedtype sequences esum exp.
 Require Import measure lebesgue_measure numfun lebesgue_integral itv kernel.
 Require Import charge prob_lang lang_syntax_util.
-From mathcomp Require Import ring lra.
+From mathcomp Require Import lra.
 
 (**md**************************************************************************)
 (* # Syntax and Evaluation for a Probabilistic Programming Language           *)
@@ -844,7 +844,7 @@ Definition mtyp t : measurableType (mtyp_disp t) :=
   projT2 (measurable_of_typ t).
 
 Definition measurable_of_seq (l : seq typ) : {d & measurableType d} :=
-  iter_mprod (map measurable_of_typ l).
+  iter_mprod (List.map measurable_of_typ l).
 
 End syntax_of_types.
 Arguments measurable_of_typ {R}.
diff --git a/theories/lang_syntax_examples.v b/theories/lang_syntax_examples.v
index 788a800726..b9c5f5a3bb 100644
--- a/theories/lang_syntax_examples.v
+++ b/theories/lang_syntax_examples.v
@@ -1,12 +1,14 @@
 Require Import String.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import mathcomp_extra boolp.
+From mathcomp Require Import ring.
+From mathcomp Require Import classical_sets.
 From mathcomp.classical Require Import functions cardinality fsbigop.
 Require Import signed reals ereal topology normedtype sequences esum measure.
 Require Import lebesgue_measure numfun lebesgue_integral kernel prob_lang.
 Require Import lang_syntax_util lang_syntax.
-From mathcomp Require Import ring lra.
+From mathcomp Require Import lra.
 
 (**md**************************************************************************)
 (* # Examples using the Probabilistic Programming Language of lang_syntax.v   *)
diff --git a/theories/prob_lang.v b/theories/prob_lang.v
index 73e831df99..ad3a69d72b 100644
--- a/theories/prob_lang.v
+++ b/theories/prob_lang.v
@@ -6,7 +6,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From mathcomp Require Import functions cardinality fsbigop.
 Require Import reals ereal signed topology normedtype sequences esum measure.
 Require Import lebesgue_measure numfun lebesgue_integral exp kernel.
-From mathcomp Require Import ring lra.
+From mathcomp Require Import lra.
 
 (**md**************************************************************************)
 (* # Semantics of a probabilistic programming language using s-finite kernels *)