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/closed') diff --git a/test-suite/bugs/closed/3755.v b/test-suite/bugs/closed/3755.v new file mode 100644 index 000000000..77427ace5 --- /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