From 20831b39a73ebd38336f19ad4ddb4d6b1078d60d Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 31 Mar 2020 20:25:05 +0200
Subject: Compiles with Coq-8.10

---
 src/lfsc/ast.ml        | 4 ++--
 src/lfsc/builtin.ml    | 2 +-
 src/lfsc/shashcons.mli | 2 ++
 3 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'src/lfsc')

diff --git a/src/lfsc/ast.ml b/src/lfsc/ast.ml
index 454bc0a..36c2f79 100644
--- a/src/lfsc/ast.ml
+++ b/src/lfsc/ast.ml
@@ -198,7 +198,7 @@ let compare_symbol s1 s2 = match s1.sname, s2.sname with
   | Name n1, Name n2 -> Hstring.compare n1 n2
   | Name _, _ -> -1
   | _, Name _ -> 1
-  | S_Hole i1, S_Hole i2 -> Pervasives.compare i1 i2
+  | S_Hole i1, S_Hole i2 -> Stdlib.compare i1 i2
 
 
 let rec compare_term ?(mod_eq=false) t1 t2 = match t1.value, t2.value with
@@ -250,7 +250,7 @@ let rec compare_term ?(mod_eq=false) t1 t2 = match t1.value, t2.value with
   | SideCond (_, _, _, t), _ -> compare_term ~mod_eq t t2
   | _, SideCond (_, _, _, t) -> compare_term ~mod_eq t1 t
 
-  | Hole i1, Hole i2 -> Pervasives.compare i1 i2
+  | Hole i1, Hole i2 -> Stdlib.compare i1 i2
 
 
 and compare_term_list ?(mod_eq=false) l1 l2 = match l1, l2 with
diff --git a/src/lfsc/builtin.ml b/src/lfsc/builtin.ml
index 86899df..75ea11e 100644
--- a/src/lfsc/builtin.ml
+++ b/src/lfsc/builtin.ml
@@ -616,7 +616,7 @@ let cong s1 s2 a1 b1 a2 b2 u1 u2 =
 
 module MInt = Map.Make (struct
     type t = int
-    let compare = Pervasives.compare
+    let compare = Stdlib.compare
   end)
 
 module STerm = Set.Make (Term)
diff --git a/src/lfsc/shashcons.mli b/src/lfsc/shashcons.mli
index 049ec5f..ca46efa 100644
--- a/src/lfsc/shashcons.mli
+++ b/src/lfsc/shashcons.mli
@@ -47,6 +47,7 @@ module type S =
 
     val iter : (t -> unit) -> unit
       (** [iter f] iterates [f] over all elements of the table . *)
+
     val stats : unit -> int * int * int * int * int * int
       (** Return statistics on the table.  The numbers are, in order:
 	  table length, number of entries, sum of bucket lengths,
@@ -83,6 +84,7 @@ module type S_consed =
 
     val iter : (key hash_consed -> unit) -> unit
       (** [iter f] iterates [f] over all elements of the table . *)
+
     val stats : unit -> int * int * int * int * int * int
       (** Return statistics on the table.  The numbers are, in order:
 	  table length, number of entries, sum of bucket lengths,
-- 
cgit