diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-10-10 16:54:37 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-10-10 16:54:37 +0200 |
| commit | 8d4037118be3ffb7259ed03a5ba4ae09d9b51f4a (patch) | |
| tree | 69b1ba6bbfeee1fa0b0f6ed847092d60a48e2f70 /src/versions/standard/Array/PArray_standard.v | |
| parent | a6cd7db941af0d41932fafc8104c3ee142b1c6f7 (diff) | |
| download | smtcoq-8d4037118be3ffb7259ed03a5ba4ae09d9b51f4a.tar.gz smtcoq-8d4037118be3ffb7259ed03a5ba4ae09d9b51f4a.zip | |
Some proofs for the Int63 glue
Diffstat (limited to 'src/versions/standard/Array/PArray_standard.v')
| -rw-r--r-- | src/versions/standard/Array/PArray_standard.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index 373e8af..2cc8366 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -21,9 +21,6 @@ Require Import Int31. Require Export Int63. -(* Require Export Int63. *) -(* Require Import Ring63. *) -(* Require Int63Lib. *) Require FMapAVL. Local Open Scope int63_scope. @@ -270,7 +267,6 @@ Proof. assert (i < length t = true). rewrite ltb_leb_sub1;auto. apply H;trivial. - rewrite <-(to_Z_add_1 _ _ H4), of_to_Z in H3;auto. exact H1. Qed. @@ -394,3 +390,10 @@ Proof. intros i _; rewrite <- (reflect_iff _ _ (HA _ _));trivial. rewrite <- not_true_iff_false, <- (reflect_iff _ _ (HA _ _)) in H0;apply H0;trivial. Qed. + + +(* + Local Variables: + coq-load-path: ((rec "../../.." "SMTCoq")) + End: +*) |