From ff9b5494cb1943339543eeac41683a8ec2dda437 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 10 Feb 2015 18:41:46 +0100 Subject: More on the support for standard Coq (not working yet) --- src/versions/standard/Array/PArray_standard.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src/versions/standard/Array/PArray_standard.v') 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. -- cgit