diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-10 18:41:46 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-10 18:41:46 +0100 |
| commit | ff9b5494cb1943339543eeac41683a8ec2dda437 (patch) | |
| tree | 21af4c0fff64fbd03c6c2006da1e305e849ebbff /src/versions/standard/Array/PArray_standard.v | |
| parent | 5311b1fa064949089b8d17e34eb31a62426f71fd (diff) | |
| download | smtcoq-ff9b5494cb1943339543eeac41683a8ec2dda437.tar.gz smtcoq-ff9b5494cb1943339543eeac41683a8ec2dda437.zip | |
More on the support for standard Coq (not working yet)
Diffstat (limited to 'src/versions/standard/Array/PArray_standard.v')
| -rw-r--r-- | src/versions/standard/Array/PArray_standard.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index ddbe0ab..069c159 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -19,9 +19,11 @@ trees *) +Require Import Int31. Require Export Int63. -Require Import Ring63. -Require Int63Lib. +(* Require Export Int63. *) +(* Require Import Ring63. *) +(* Require Int63Lib. *) Require FMapAVL. Local Open Scope int63_scope. @@ -87,7 +89,7 @@ Local Open Scope array_scope. Set Vm Optimize. -Definition max_array_length := Eval vm_compute in (Int63Lib.phi_inv 4194302). +Definition max_array_length := 4194302%int31. (** Axioms *) Axiom get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t. |