diff options
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/Inductive.v | 17 | ||||
-rw-r--r-- | test-suite/success/polymorphism.v | 46 | ||||
-rw-r--r-- | test-suite/success/qed_export.v | 18 |
3 files changed, 63 insertions, 18 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index f746def5c..06f807f29 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -183,3 +183,20 @@ Module PolyNoLowerProp. Fail Check Foo True : Prop. End PolyNoLowerProp. + +(* Test building of elimination scheme with noth let-ins and + non-recursively uniform parameters *) + +Module NonRecLetIn. + + Unset Implicit Arguments. + + Inductive Ind (b:=2) (a:nat) (c:=1) : Type := + | Base : Ind a + | Rec : Ind (S a) -> Ind a. + + Check Ind_rect (fun n (b:Ind n) => b = b) + (fun n => eq_refl) + (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). + +End NonRecLetIn. diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index ecc988507..7eaafc354 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -156,6 +156,52 @@ Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d. End structures. + +Module binders. + + Definition mynat@{|} := nat. + + Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}. + exact A. + Defined. + + Definition nomoreu@{i j | i < j +} (A : Type@{i}) : Type@{j}. + pose(foo:=Type). + exact A. + Fail Defined. + Abort. + + Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}. + pose(foo:=Type). + exact A. + Defined. + + Check moreu@{_ _ _ _}. + + Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A. + + (* By default constraints are extensible *) + Polymorphic Definition morec@{i j} (A : Type@{i}) : Type@{j} := A. + Check morec@{_ _}. + + (* Handled in proofs as well *) + Lemma bar@{i j | } : Type@{i}. + exact Type@{j}. + Fail Defined. + Abort. + + Lemma bar@{i j| i < j} : Type@{j}. + Proof. + exact Type@{i}. + Qed. + + Lemma barext@{i j|+} : Type@{j}. + Proof. + exact Type@{i}. + Qed. + +End binders. + Section cats. Local Set Universe Polymorphism. Require Import Utf8. diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v deleted file mode 100644 index b3e41ab1f..000000000 --- a/test-suite/success/qed_export.v +++ /dev/null @@ -1,18 +0,0 @@ -Lemma a : True. -Proof. -assert True as H. - abstract (trivial) using exported_seff. -exact H. -Fail Qed exporting a_subproof. -Qed exporting exported_seff. -Check ( exported_seff : True ). - -Lemma b : True. -Proof. -assert True as H. - abstract (trivial) using exported_seff2. -exact H. -Qed. - -Fail Check ( exported_seff2 : True ). - |