From e1f5a499c43ec0d7b7ebe696941217fb503e2596 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Jul 2015 16:09:29 +0200 Subject: Kernel: primitive projections handling of let-ins Fixes bug #4176 (actually two bugs in one) Correct computation of the type of primitive projections in presence of let-ins. --- test-suite/bugs/closed/4276.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/4276.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4276.v b/test-suite/bugs/closed/4276.v new file mode 100644 index 0000000000..ba82e6c376 --- /dev/null +++ b/test-suite/bugs/closed/4276.v @@ -0,0 +1,11 @@ +Set Primitive Projections. + +Record box (T U : Type) (x := T) := wrap { unwrap : T }. +Definition mybox : box True False := wrap _ _ I. +Definition unwrap' := @unwrap. + +Definition bad' : True := mybox.(unwrap _ _). + +Fail Definition bad : False := unwrap _ _ mybox. + +(* Closed under the global context *) \ No newline at end of file -- cgit v1.2.3 From 2c59d19ad207a6bf193e9f0c9d73258b3133d484 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Jul 2015 16:58:06 +0200 Subject: Kernel/Checker: Cleanup fixes of substitutions due to let-ins. Avoid undeeded large substitutions, and add test-suite file for fixed bug 4283 in closed/ --- test-suite/bugs/closed/4283.v | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 test-suite/bugs/closed/4283.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4283.v b/test-suite/bugs/closed/4283.v new file mode 100644 index 0000000000..e06998b711 --- /dev/null +++ b/test-suite/bugs/closed/4283.v @@ -0,0 +1,8 @@ +Require Import Hurkens. + +Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. + +Definition unwrap' := fun (X : Type) (b : box X) => let (unwrap) := b in unwrap. + +Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl. + -- cgit v1.2.3 From 6a15394c542e5f16bce9b75fc033397c454f47e9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 16 Jul 2015 19:24:23 +0200 Subject: Test file for #3819. --- test-suite/bugs/closed/3819.v | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 test-suite/bugs/closed/3819.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/3819.v b/test-suite/bugs/closed/3819.v new file mode 100644 index 0000000000..355d23a58b --- /dev/null +++ b/test-suite/bugs/closed/3819.v @@ -0,0 +1,9 @@ +Record Op := { t : Type ; op : t -> t }. + +Canonical Structure OpType : Op := Build_Op Type (fun X => X). + +Lemma test1 (X:Type) : eq (op OpType X) X. +Proof eq_refl. + +Definition test2 (A:Type) : eq (op _ A) A. +Proof eq_refl. \ No newline at end of file -- cgit v1.2.3 From 8591217a89f0b71e8175752dc55c42a5b89fccec Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 20:21:58 +0200 Subject: Fixing bug #4240 (closure_of_filter was not ensuring refinement of former filter after 48509b61 and 3cd718c, because filtered let-ins were not any longer preserved). --- test-suite/bugs/closed/4240.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 test-suite/bugs/closed/4240.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4240.v b/test-suite/bugs/closed/4240.v new file mode 100644 index 0000000000..083c59fe68 --- /dev/null +++ b/test-suite/bugs/closed/4240.v @@ -0,0 +1,12 @@ +(* Check that closure of filter did not restrict the former evar filter *) + +Lemma foo (new : nat) : False. +evar (H1: nat). +set (H3 := 0). +assert (H3' := id H3). +evar (H5: nat). +clear H3. +assert (H5 = new). +unfold H5. +unfold H1. +exact (eq_refl new). -- cgit v1.2.3 From 916a8dc2c6b1dd8400d5c44b5d9c7fc793cc0e97 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 16 Jul 2015 21:40:42 +0200 Subject: Remove old test file for #3819 (now fixed). --- test-suite/bugs/opened/3819.v | 11 ----------- 1 file changed, 11 deletions(-) delete mode 100644 test-suite/bugs/opened/3819.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/opened/3819.v deleted file mode 100644 index 7105a65877..0000000000 --- a/test-suite/bugs/opened/3819.v +++ /dev/null @@ -1,11 +0,0 @@ -Set Universe Polymorphism. - -Record Op := { t : Type ; op : t -> t }. - -Canonical Structure OpType : Op := Build_Op Type (fun X => X). - -Lemma test1 (X:Type) : eq (op OpType X) X. -Proof eq_refl. - -Lemma test2 (A:Type) : eq (op _ A) A. -Fail Proof eq_refl. -- cgit v1.2.3 From fdd6a17b272995237c9f95fc465bb1ff6871bedc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 22:53:10 +0200 Subject: Refining 71def2f8 on too strong occur-check limiting evar-evar unification in tactics. The relaxing of occur-check was ok but was leading trivial problems of the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into ?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems was not any more able to deal with. Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way, so that it behaves as if the occur-check had not been restricted. --- test-suite/bugs/closed/4205.v | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 test-suite/bugs/closed/4205.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4205.v b/test-suite/bugs/closed/4205.v new file mode 100644 index 0000000000..c40dfcc1f3 --- /dev/null +++ b/test-suite/bugs/closed/4205.v @@ -0,0 +1,8 @@ +(* Testing a regression from 8.5beta1 to 8.5beta2 in evar-evar tactic unification problems *) + + +Inductive test : nat -> nat -> nat -> nat -> Prop := + | test1 : forall m n, test m n m n. + +Goal test 1 2 3 4. +erewrite f_equal2 with (f := fun k l => test _ _ k l). -- cgit v1.2.3