From e3764e1e857fce9b6d4cb018db676db3612c00a0 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 31 Aug 2020 08:52:05 +0200 Subject: Remove occurrences of Parray.reroot. --- theories/Array/PArray.v | 19 ------------------- 1 file changed, 19 deletions(-) (limited to 'theories/Array/PArray.v') diff --git a/theories/Array/PArray.v b/theories/Array/PArray.v index 3511ba0918..e91a5bf9ad 100644 --- a/theories/Array/PArray.v +++ b/theories/Array/PArray.v @@ -22,12 +22,6 @@ Arguments length {_} _. Primitive copy : forall A, array A -> array A := #array_copy. Arguments copy {_} _. -(* [reroot t] produces an array that is extensionaly equal to [t], but whose - history has been squashed. Useful when performing multiple accesses in an old - copy of an array that has been updated. *) -Primitive reroot : forall A, array A -> array A := #array_reroot. -Arguments reroot {_} _. - Module Export PArrayNotations. Declare Scope array_scope. @@ -64,9 +58,6 @@ Axiom length_set : forall A t i (a:A), Axiom get_copy : forall A (t:array A) i, (copy t).[i] = t.[i]. Axiom length_copy : forall A (t:array A), length (copy t) = length t. -Axiom get_reroot : forall A (t:array A) i, (reroot t).[i] = t.[i]. -Axiom length_reroot : forall A (t:array A), length (reroot t) = length t. - Axiom array_ext : forall A (t1 t2:array A), length t1 = length t2 -> (forall i, i t1.[i] = t2.[i]) -> @@ -94,16 +85,6 @@ Proof. rewrite !get_out_of_bounds in get_make; assumption. Qed. -Lemma default_reroot A (t:array A) : default (reroot t) = default t. -Proof. - assert (irr_lt : length t