Ssreflect Users Discussion List

[Georges Gonthier <>]

   While the code was accepted in 8.4, I suspect it did not have the intended 
semantics, and that Coq simply ignored the predArgType annotation in the 
Structure declaration, as this was the case in earlier versions, and that 
this was "fixed" in 8.5 by trying to equate the sort imposed by the 
Record/structure code with the declared one - whence your error.
   Possible workarounds:
 - Use Inductive to declare your type, and define the coercion to nat * nat 
explicitly. You will not be able to infer canonical box_ins if you do this, 
though. This is what the mathcomp library does for ordinal.
- Replace the predArgType annotation with Type. You will need to use the {: 
box_in sh} notation when you want to use box_in as a collection (e.g., in 
#|{: box_in sh}| = sumn sh).
- Define box_in : predArgType := box_in_struct, where box_in_struct is your 
declared Structure. Note that the "internal" box_in_struct type will then 
appear in the type of coord and BoxIn.

   Thus, there are no perfect solutions; you should also probably report a 
Coq bug.

Cheers,
   Georges
 
-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Florent Hivert
Sent: 14 March 2016 17:14
To: 

Subject: [ssreflect] Universe inconsistency with coq 8.5

      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}.