diff options
| author | Vincent Laporte | 2020-03-20 08:33:07 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2020-03-20 08:33:07 +0100 |
| commit | d2e29e64603edd28140935f01f82936e9eeff8c8 (patch) | |
| tree | e3c13607b9a83b50f8864f9d869845d66852fef6 /plugins/micromega/mutils.ml | |
| parent | 47d92a69773755e2ad5d5f987f87337fdf7e98d8 (diff) | |
| parent | 1dcd622c45ad8880492d115af9ad8d333a62738e (diff) | |
Merge PR #11857: Remove calls to structural equality in Micromega
Reviewed-by: vbgl
Diffstat (limited to 'plugins/micromega/mutils.ml')
| -rw-r--r-- | plugins/micromega/mutils.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index f9a23751bf..27b917383b 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -385,7 +385,13 @@ module Hash = struct let int_of_eq_op1 = Mc.(function Equal -> 0 | NonEqual -> 1 | Strict -> 2 | NonStrict -> 3) - let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2 + let int_of_eq_op2 = + Mc.( + function + | OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5) + + let eq_op1 o1 o2 = Int.equal (int_of_eq_op1 o1) (int_of_eq_op1 o2) + let eq_op2 o1 o2 = Int.equal (int_of_eq_op2 o1) (int_of_eq_op2 o2) let hash_op1 h o = combine h (int_of_eq_op1 o) let rec eq_positive p1 p2 = |