From ea083ac106f048e64c1b57ddd37ac717236b8ecd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 14 Feb 2015 12:54:36 +0100 Subject: Univs: When computing the level of an inductive including indices, lets do not contribute. Fixes bug #3808. --- test-suite/bugs/closed/3808.v | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 test-suite/bugs/closed/3808.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v new file mode 100644 index 0000000000..6e19ddf8dc --- /dev/null +++ b/test-suite/bugs/closed/3808.v @@ -0,0 +1,2 @@ +Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i}) + := foo : Foo. \ No newline at end of file -- cgit v1.2.3 From 40072e20736198485fa5381c6af4dd8c87a077da Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 14 Feb 2015 13:32:29 +0100 Subject: Univs: fix bug #3755. We were missing refreshements of universes in unifications ?X ~= ?Y foo not catched by solve_evar_evar. --- test-suite/bugs/closed/3755.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 test-suite/bugs/closed/3755.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/3755.v b/test-suite/bugs/closed/3755.v new file mode 100644 index 0000000000..77427ace58 --- /dev/null +++ b/test-suite/bugs/closed/3755.v @@ -0,0 +1,16 @@ +(* File reduced by coq-bug-finder from original input, then from 6729 lines to +411 lines, then from 148 lines to 115 lines, then from 99 lines to 70 lines, +then from 85 lines to 63 lines, then from 76 lines to 55 lines, then from 61 +lines to 17 lines *) +(* coqc version trunk (January 2015) compiled on Jan 17 2015 21:58:5 with OCaml +4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk +(9e6b28c04ad98369a012faf3bd4d630cf123a473) *) +Set Printing Universes. +Section param. + Variable typeD : Set -> Set. + Variable STex : forall (T : Type) (p : T -> Set), Set. + Definition existsEach_cons' v (P : @sigT _ typeD -> Set) := + @STex _ (fun x => P (@existT _ _ v x)). + + Check @existT _ _ STex STex. -- cgit v1.2.3 From 93862f2ab93ec3fab3549c868706bc247422674b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 14 Feb 2015 16:09:16 +0100 Subject: Test for bug #4016. --- test-suite/bugs/closed/4016.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 test-suite/bugs/closed/4016.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4016.v b/test-suite/bugs/closed/4016.v new file mode 100644 index 0000000000..41cb1a8884 --- /dev/null +++ b/test-suite/bugs/closed/4016.v @@ -0,0 +1,12 @@ +Require Import Setoid. + +Parameter eq : relation nat. +Declare Instance Equivalence_eq : Equivalence eq. + +Lemma foo : forall z, eq z 0 -> forall x, eq x 0 -> eq z x. +Proof. +intros z Hz x Hx. +rewrite <- Hx in Hz. +destruct z. +Abort. + -- cgit v1.2.3 From f9c2d5d26a6a8e15549ada1f69d630acfa1a9437 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Feb 2015 13:39:27 +0100 Subject: Fixing test-suite. --- test-suite/bugs/closed/4017.v | 2 ++ test-suite/bugs/closed/4018.v | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v index a6f177b496..aa810f4f0e 100644 --- a/test-suite/bugs/closed/4017.v +++ b/test-suite/bugs/closed/4017.v @@ -1,3 +1,5 @@ +Set Implicit Arguments. + (* Use of implicit arguments was lost in multiple variable declarations *) Variables (A1 : Type) diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v index c3a045943c..8895e09e02 100644 --- a/test-suite/bugs/closed/4018.v +++ b/test-suite/bugs/closed/4018.v @@ -1,3 +1,3 @@ (* Catching PatternMatchingFailure was lost at some point *) Goal nat -> True. -intros [=]. +Fail intros [=]. -- cgit v1.2.3 From 6a844a236ccef9efb2fb6f86ecba8a6a182a4034 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Feb 2015 13:57:36 +0100 Subject: Test for bug #3916. --- test-suite/bugs/closed/3916.v | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test-suite/bugs/closed/3916.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/3916.v b/test-suite/bugs/closed/3916.v new file mode 100644 index 0000000000..55c3a35c3a --- /dev/null +++ b/test-suite/bugs/closed/3916.v @@ -0,0 +1,3 @@ +Require Import List. +Fail Hint Resolve -> in_map. + -- cgit v1.2.3 From 362b7ef4422b451e621ca8400692de1decb0503d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Feb 2015 14:08:04 +0100 Subject: Test for bug #3490. --- test-suite/bugs/closed/3490.v | 27 +++++++++++++++++++++++++++ test-suite/bugs/opened/3490.v | 27 --------------------------- 2 files changed, 27 insertions(+), 27 deletions(-) create mode 100644 test-suite/bugs/closed/3490.v delete mode 100644 test-suite/bugs/opened/3490.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/3490.v b/test-suite/bugs/closed/3490.v new file mode 100644 index 0000000000..e7a5caa1de --- /dev/null +++ b/test-suite/bugs/closed/3490.v @@ -0,0 +1,27 @@ +Inductive T : Type := +| Var : nat -> T +| Arr : T -> T -> T. + +Inductive Tele : list T -> Type := +| Tnil : @Tele nil +| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). + +Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t} + : { x : Type & x -> nat -> Type } := + match t return { x : Type & x -> nat -> Type } with + | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit) + | Tcons ls t' l => + let (result, get) := TeleD ls t' in + @existT Type (fun x => x -> nat -> Type) + { v : result & (fix TD (t : T) {struct t} := + match t with + | Var n => + get v n + | Arr a b => TD a -> TD b + end) l } + (fun x n => + match n return Type with + | 0 => projT2 x + | S n => get (projT1 x) n + end) + end. diff --git a/test-suite/bugs/opened/3490.v b/test-suite/bugs/opened/3490.v deleted file mode 100644 index e7a5caa1de..0000000000 --- a/test-suite/bugs/opened/3490.v +++ /dev/null @@ -1,27 +0,0 @@ -Inductive T : Type := -| Var : nat -> T -| Arr : T -> T -> T. - -Inductive Tele : list T -> Type := -| Tnil : @Tele nil -| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). - -Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t} - : { x : Type & x -> nat -> Type } := - match t return { x : Type & x -> nat -> Type } with - | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit) - | Tcons ls t' l => - let (result, get) := TeleD ls t' in - @existT Type (fun x => x -> nat -> Type) - { v : result & (fix TD (t : T) {struct t} := - match t with - | Var n => - get v n - | Arr a b => TD a -> TD b - end) l } - (fun x n => - match n return Type with - | 0 => projT2 x - | S n => get (projT1 x) n - end) - end. -- cgit v1.2.3 From aed3c876d422f4dcc0296fd4949148c697f37b1d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 15 Feb 2015 18:13:04 +0100 Subject: Fix test-suite file. Check that definitions do work when sharing is disabled in the kernel. --- test-suite/bugs/closed/3309.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v index 9e12b990b7..049589325e 100644 --- a/test-suite/bugs/closed/3309.v +++ b/test-suite/bugs/closed/3309.v @@ -315,8 +315,6 @@ Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) : hrel (@setq intros; exact (@quotrel _ _). Defined. -(* Unset Kernel Term Sharing. *) - Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit. Definition ispartlbinopabmonoidfracrel_type : Type := @@ -326,3 +324,10 @@ Definition ispartlbinopabmonoidfracrel_type : Type := Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in ispartlbinopabmonoidfracrel_type in exact t)$. +Unset Kernel Term Sharing. + +Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit. + +Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in + ispartlbinopabmonoidfracrel_type in exact t)$. + -- cgit v1.2.3