diff options
| author | Guillaume Melquiond | 2020-08-31 08:52:05 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-10-08 11:16:48 +0200 |
| commit | e3764e1e857fce9b6d4cb018db676db3612c00a0 (patch) | |
| tree | 2972e326e1ec69b017c0789939d8faf481d01758 /test-suite/primitive | |
| parent | ddd7371dc3b82124c2bb36b93e6c2b185bcc02d2 (diff) | |
Remove occurrences of Parray.reroot.
Diffstat (limited to 'test-suite/primitive')
| -rw-r--r-- | test-suite/primitive/arrays/reroot.v | 22 |
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). |
