diff options
| author | Jasper Hugunin | 2020-09-09 12:53:52 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | d9ce5d4a8c3cd252a50529074455b07737679746 (patch) | |
| tree | 8f0b6411b8aee04dfb4801bc699e6d827999591a | |
| parent | d0aea47877be293f96e4662824c5d4728c8334b7 (diff) | |
Modify Arith/Between.v to compile with -mangle-names
| -rw-r--r-- | theories/Arith/Between.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 1db3f87cac..74d1e391c4 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -110,7 +110,7 @@ Section Between. Lemma between_in_int : forall k l, between k l -> forall r, in_int k l r -> P r. Proof. - induction 1; intros. + intro k; induction 1 as [|l]; intros r ?. - absurd (k < k). { auto with arith. } eapply in_int_lt; eassumption. - destruct (in_int_p_Sq k l r) as [| ->]; auto with arith. @@ -125,7 +125,7 @@ Section Between. Lemma exists_in_int : forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. Proof. - induction 1 as [* ? (p, ?, ?)|]. + induction 1 as [* ? (p, ?, ?)|l]. - exists p; auto with arith. - exists l; auto with arith. Qed. @@ -154,7 +154,7 @@ Section Between. between k l -> (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l. Proof. - induction 1; red; intros. + intro k; induction 1 as [|l]; red; intros. - absurd (k < k); auto with arith. - absurd (Q l). { auto with arith. } destruct (exists_in_int k (S l)) as (l',[],?). |