diff options
| author | Gaëtan Gilbert | 2018-07-10 15:34:22 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 13:49:18 +0200 |
| commit | 277563ab74a0529c330343479a063f808baa6db4 (patch) | |
| tree | 32dde6c28e260af4fa9b6d716cf27c01e97ba347 | |
| parent | 076bb351257dfd3c605c010d95484f224bef5e56 (diff) | |
Add simple test cases for vm and native on primitive projections.
| -rw-r--r-- | test-suite/success/primitiveproj.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 7ca2767a53..299b08bdd1 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -193,12 +193,13 @@ Set Primitive Projections. Record s (x:nat) (y:=S x) := {c:=x; d:x=c}. Lemma f : 0=1. Proof. -Fail apply d. + Fail apply d. (* split. reflexivity. Qed. *) +Abort. (* Primitive projection match compilation *) Require Import List. @@ -220,3 +221,9 @@ Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) := Time Eval vm_compute in split_at (repeat 0 20) 10. (* Takes 0s *) Time Eval vm_compute in split_at (repeat 0 40) 20. (* Takes 0.001s *) Timeout 1 Time Eval vm_compute in split_at (repeat 0 60) 30. (* Used to take 60s, now takes 0.001s *) + +Check (@eq_refl _ 0 <: 0 = fst (pair 0 1)). +Fail Check (@eq_refl _ 0 <: 0 = snd (pair 0 1)). + +Check (@eq_refl _ 0 <<: 0 = fst (pair 0 1)). +Fail Check (@eq_refl _ 0 <<: 0 = snd (pair 0 1)). |