diff options
| -rw-r--r-- | theories/Zarith/fast_integer.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v index 444d5e9a15..93b78f9e44 100644 --- a/theories/Zarith/fast_integer.v +++ b/theories/Zarith/fast_integer.v @@ -258,7 +258,7 @@ Theorem compare_convert1 : ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL. Proof. Induction x;Induction y;Split;Simpl;Auto with arith; - (Discriminate Orelse (Elim (H y0); Auto with arith)). + (Discriminate Orelse (Elim (H p0); Auto with arith)). Save. Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y. |