diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-01 18:26:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-01 22:45:39 +0100 |
| commit | 87b510e5b0f363724eae5db9f177f167a3586015 (patch) | |
| tree | 204c7ad1e1ba38945ab58d74e28d8cf67201fe71 /plugins/rtauto | |
| parent | bca756eaebf16b6145c65b53629219d2a0a8b1ba (diff) | |
Fixing pervasive comparisons
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 101fe288b..1ed9b8269 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -69,7 +69,7 @@ module FOrd = struct | Bot, Bot -> 0 | Bot, _ -> -1 | Atom _, Bot -> 1 - | Atom a1, Atom a2 -> Pervasives.compare a1 a2 + | Atom a1, Atom a2 -> Int.compare a1 a2 | Atom _, _ -> -1 | Arrow _, (Bot | Atom _) -> 1 | Arrow (f1, g1), Arrow (f2, g2) -> |