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/ast.ml | |
| parent | 4c8654c57666e27637ba2f60ee5c6455176c7a1d (diff) | |
| download | smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.tar.gz smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.zip | |
Compiles with Coq-8.10
Diffstat (limited to 'src/lfsc/ast.ml')
| -rw-r--r-- | src/lfsc/ast.ml | 4 |
1 files changed, 2 insertions, 2 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 |