diff options
| author | Pierre-Marie Pédrot | 2017-09-06 23:46:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-06 23:46:41 +0200 |
| commit | d6997e31e7fc4cfc6e020bf1ab53e6b1fa3f74fe (patch) | |
| tree | 2245ee809915f3fa1aa1bb7d882b004c795abadc | |
| parent | 64a6ac3759b5d0ea635ff284606541b05c696996 (diff) | |
Fix coq/ltac2#23: Int.compare should not be uniformly 0.
Stupid typo.
| -rw-r--r-- | src/tac2core.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 603ddeecfd..7f136b48ae 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -230,7 +230,7 @@ let () = define2 "int_equal" int int begin fun _ m n -> end let binop n f = define2 n int int begin fun _ m n -> - return (Value.of_int (f m m)) + return (Value.of_int (f m n)) end let () = binop "int_compare" Int.compare |