Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear MathComp fans,

The following code which was perfectly working with Coq-8.4pl6 and
MathComp-1.6 is refused by switching to Coq-8.5 with a

Toplevel input, characters 15-105:
Error: Universe inconsistency. Cannot enforce Set =
mathcomp.ssreflect.ssrbool.517.

I've no idea what changed. Any suggestion or fix ?

Best,

Florent


Set Printing Universes.

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrbool ssrfun ssrnat eqtype fintype choice seq.

Set Implicit Arguments.
Unset Strict Implicit.


(** * Shapes *)
Definition is_in_shape sh r c := c < nth 0 sh r.

(** ** A finite type [finType] for coordinate of boxes inside a shape *)
Section BoxIn.

Variable sh : seq nat.

Definition is_box_in_shape b := is_in_shape sh b.1 b.2.

Structure box_in : predArgType :=
  BoxIn {coord :> nat * nat; _ : is_box_in_shape coord}.