diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v
index 0f5268a19..957d7c5e8 100644
--- a/theories/lang_syntax.v
+++ b/theories/lang_syntax.v
@@ -1,13 +1,13 @@
 Require Import String.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
+From mathcomp Require Import lra.
 From mathcomp Require Import mathcomp_extra boolp classical_sets.
 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 ftc.
-Require Import probability.
-Require Import derive realfun charge prob_lang lang_syntax_util.
-From mathcomp Require Import lra.
+From mathcomp Require Import signed reals ereal topology normedtype sequences.
+From mathcomp Require Import esum exp derive realfun measure lebesgue_measure.
+From mathcomp Require Import numfun lebesgue_integral itv kernel ftc.
+From mathcomp Require Import probability charge prob_lang lang_syntax_util.
 
 (**md**************************************************************************)
 (* # Syntax and Evaluation for a Probabilistic Programming Language           *)
diff --git a/theories/lang_syntax_examples.v b/theories/lang_syntax_examples.v
index 62afa9581..1a9f43e33 100644
--- a/theories/lang_syntax_examples.v
+++ b/theories/lang_syntax_examples.v
@@ -1,14 +1,13 @@
-Require Import String.
+From Coq 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.
-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 probability.
-Require Import prob_lang lang_syntax_util lang_syntax.
-From mathcomp Require Import lra.
+From mathcomp Require Import ring lra.
+From mathcomp Require Import classical_sets functions cardinality fsbigop.
+From mathcomp Require Import signed reals ereal topology normedtype sequences.
+From mathcomp Require Import esum measure lebesgue_measure numfun.
+From mathcomp Require Import lebesgue_integral kernel probability prob_lang.
+From mathcomp Require Import lang_syntax_util lang_syntax.
 
 (**md**************************************************************************)
 (* # Examples using the Probabilistic Programming Language of lang_syntax.v   *)
diff --git a/theories/lang_syntax_table_game.v b/theories/lang_syntax_table_game.v
index 46fc62cef..a9d6c26dd 100644
--- a/theories/lang_syntax_table_game.v
+++ b/theories/lang_syntax_table_game.v
@@ -1,13 +1,13 @@
 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 functions cardinality fsbigop.
-Require Import signed reals ereal topology normedtype sequences esum measure.
-Require Import charge lebesgue_measure numfun lebesgue_integral kernel.
-Require Import probability.
-Require Import prob_lang lang_syntax_util lang_syntax lang_syntax_examples.
 From mathcomp Require Import ring lra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
+From mathcomp Require Import functions cardinality fsbigop.
+From mathcomp Require Import signed reals ereal topology normedtype sequences.
+From mathcomp Require Import esum measure charge lebesgue_measure numfun.
+From mathcomp Require Import lebesgue_integral kernel probability prob_lang.
+From mathcomp Require Import lang_syntax_util lang_syntax lang_syntax_examples.
 
 (**md**************************************************************************)
 (* # Eddy's table game example                                                *)
diff --git a/theories/lang_syntax_toy.v b/theories/lang_syntax_toy.v
index 2c2f57267..ae6463adb 100644
--- a/theories/lang_syntax_toy.v
+++ b/theories/lang_syntax_toy.v
@@ -1,9 +1,9 @@
-Require Import String Classical.
+From Coq Require Import String Classical.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg.
 From mathcomp Require Import mathcomp_extra boolp.
-Require Import signed reals topology normedtype.
-Require Import lang_syntax_util.
+From mathcomp Require Import signed reals topology normedtype.
+From mathcomp Require Import lang_syntax_util.
 
 (******************************************************************************)
 (*           Intrinsically-typed concrete syntax for a toy language           *)
diff --git a/theories/lang_syntax_util.v b/theories/lang_syntax_util.v
index 608d25e7e..253c1d8ff 100644
--- a/theories/lang_syntax_util.v
+++ b/theories/lang_syntax_util.v
@@ -1,8 +1,8 @@
-Require Import String.
+From Coq Require Import String.
 From HB Require Import structures.
 Require Import Classical_Prop. (* NB: to compile with Coq 8.17 *)
 From mathcomp Require Import all_ssreflect.
-Require Import signed.
+From mathcomp Require Import signed.
 
 (******************************************************************************)
 (*                  Shared by lang_syntax_*.v files                           *)
diff --git a/theories/prob_lang.v b/theories/prob_lang.v
index fceadacfb..e009899ed 100644
--- a/theories/prob_lang.v
+++ b/theories/prob_lang.v
@@ -2,12 +2,12 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import rat archimedean.
+From mathcomp Require Import lra.
 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.
-Require Import probability.
-From mathcomp Require Import lra.
+From mathcomp Require Import reals ereal signed topology normedtype sequences.
+From mathcomp Require Import esum measure lebesgue_measure numfun.
+From mathcomp Require Import lebesgue_integral exp kernel probability.
 
 (**md**************************************************************************)
 (* # Semantics of a probabilistic programming language using s-finite kernels *)
diff --git a/theories/prob_lang_wip.v b/theories/prob_lang_wip.v
index 8a7bedb31..f2e247835 100644
--- a/theories/prob_lang_wip.v
+++ b/theories/prob_lang_wip.v
@@ -3,9 +3,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop.
-Require Import signed reals ereal topology normedtype sequences esum measure.
-Require Import lebesgue_measure numfun lebesgue_integral exp kernel trigo.
-Require Import realfun charge prob_lang.
+From mathcomp Require Import signed reals ereal topology normedtype sequences.
+From mathcomp Require Import esum measure lebesgue_measure numfun exp trigo.
+From mathcomp Require Import realfun lebesgue_integral kernel charge prob_lang.
 
 (******************************************************************************)
 (*  Semantics of a probabilistic programming language using s-finite kernels  *)