diff options
| author | Jasper Hugunin | 2020-09-12 17:11:36 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | 1a0017b8b85d2536d333f6b85f311aefa219b33a (patch) | |
| tree | 6a93b553f4f7afc0e6fe8bc86ea038841c216775 | |
| parent | 0f6f3eedb65c3b061b4d4443c18e57ad38bb1f41 (diff) | |
Modify Arith/Compare_dec.v to compile with -mangle-names
| -rw-r--r-- | theories/Arith/Compare_dec.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 341dd7de5d..1afc49b7ff 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -21,7 +21,7 @@ Defined. Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. Proof. - induction n in m |- *; destruct m; auto with arith. + induction n as [|n IHn] in m |- *; destruct m as [|m]; auto with arith. destruct (IHn m) as [H|H]; auto with arith. destruct H; auto with arith. Defined. @@ -33,9 +33,9 @@ Defined. Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. - induction n in m |- *. + induction n as [|n IHn] in m |- *. - left; auto with arith. - - destruct m. + - destruct m as [|m]. + right; auto with arith. + elim (IHn m); [left|right]; auto with arith. Defined. |