From 041e5eef89b1db909f076494204eda2c20562bb8 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 3 Oct 2017 10:49:12 +0200 Subject: Compiles with Coq-8.6 --- src/versions/standard/Array/PArray_standard.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'src/versions/standard/Array') diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index 2cc8366..4bf5e7a 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -80,8 +80,6 @@ Notation "t '.[' i '<-' a ']'" := (set t i a) (at level 50) : array_scope. Local Open Scope array_scope. -Set Vm Optimize. - Definition max_array_length := 4194302%int31. (** Axioms *) -- cgit