aboutsummaryrefslogtreecommitdiff
path: root/test-suite/primitive
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-08-31 08:52:05 +0200
committerGuillaume Melquiond2020-10-08 11:16:48 +0200
commite3764e1e857fce9b6d4cb018db676db3612c00a0 (patch)
tree2972e326e1ec69b017c0789939d8faf481d01758 /test-suite/primitive
parentddd7371dc3b82124c2bb36b93e6c2b185bcc02d2 (diff)
Remove occurrences of Parray.reroot.
Diffstat (limited to 'test-suite/primitive')
-rw-r--r--test-suite/primitive/arrays/reroot.v22
1 files changed, 0 insertions, 22 deletions
diff --git a/test-suite/primitive/arrays/reroot.v b/test-suite/primitive/arrays/reroot.v
deleted file mode 100644
index 172a118cc7..0000000000
--- a/test-suite/primitive/arrays/reroot.v
+++ /dev/null
@@ -1,22 +0,0 @@
-From Coq Require Import Int63 PArray.
-
-Open Scope array_scope.
-
-Definition t : array nat := [| 1; 5; 2 | 4 |].
-Definition t' : array nat := PArray.reroot t.
-
-Definition foo1 := (eq_refl : t'.[1] = 5).
-Definition foo2 := (eq_refl 5 <: t'.[1] = 5).
-Definition foo3 := (eq_refl 5 <<: t'.[1] = 5).
-Definition x1 := Eval compute in t'.[1].
-Definition foo4 := (eq_refl : x1 = 5).
-Definition x2 := Eval cbn in t'.[1].
-Definition foo5 := (eq_refl : x2 = 5).
-
-Definition foo6 := (eq_refl : t.[1] = 5).
-Definition foo7 := (eq_refl 5 <: t.[1] = 5).
-Definition foo8 := (eq_refl 5 <<: t.[1] = 5).
-Definition x3 := Eval compute in t.[1].
-Definition foo9 := (eq_refl : x3 = 5).
-Definition x4 := Eval cbn in t.[1].
-Definition foo10 := (eq_refl : x4 = 5).