diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-03-31 20:25:05 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-03-31 20:25:05 +0200 |
| commit | 20831b39a73ebd38336f19ad4ddb4d6b1078d60d (patch) | |
| tree | 9e4ec27753feff8f7e95274f99eaa977b546c030 /src/lfsc | |
| parent | 4c8654c57666e27637ba2f60ee5c6455176c7a1d (diff) | |
| download | smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.tar.gz smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.zip | |
Compiles with Coq-8.10
Diffstat (limited to 'src/lfsc')
| -rw-r--r-- | src/lfsc/ast.ml | 4 | ||||
| -rw-r--r-- | src/lfsc/builtin.ml | 2 | ||||
| -rw-r--r-- | src/lfsc/shashcons.mli | 2 |
3 files changed, 5 insertions, 3 deletions
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, |