diff options
| author | Jasper Hugunin | 2020-09-12 17:13:21 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | c82bea6f76ad0b6ea57cda027cc49ec009850a48 (patch) | |
| tree | 7ac5c12a03b996d4c75d3b16b89989a364de7fc8 | |
| parent | 1a0017b8b85d2536d333f6b85f311aefa219b33a (diff) | |
Modify Arith/Factorial.v to compile with -mangle-names
| -rw-r--r-- | theories/Arith/Factorial.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 0871c4af67..f87d7e810a 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -33,7 +33,7 @@ Qed. Lemma fact_le n m : n <= m -> fact n <= fact m. Proof. - induction 1. + induction 1 as [|m ?]. - apply le_n. - simpl. transitivity (fact m). trivial. apply Nat.le_add_r. Qed. |