diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-02-14 13:32:29 +0100 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-02-14 13:32:29 +0100 |
commit | 40072e20736198485fa5381c6af4dd8c87a077da (patch) | |
tree | e8d83b553cf18d20c786f49ab11cb6ad48c4fb54 /test-suite/bugs/closed/3755.v | |
parent | ea083ac106f048e64c1b57ddd37ac717236b8ecd (diff) |
Univs: fix bug #3755. We were missing refreshements of universes in
unifications ?X ~= ?Y foo not catched by solve_evar_evar.
Diffstat (limited to 'test-suite/bugs/closed/3755.v')
-rw-r--r-- | test-suite/bugs/closed/3755.v | 16 |
1 files changed, 16 insertions, 0 deletions
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. |