search

math-comp / math-comp

Mathematical Components
https://math-comp.github.io
587 stars 115 forks source link

Type inference for subtype #888

Open thery opened 2 years ago

thery commented 2 years ago

while porting some files from a tutorial by assia (here) It seems that before we could write

Definition two'' : 'I_3 := Sub 2 (refl_equal true).

but now we have to write.

Definition two'' : [subType of 'I_3] := Sub 2 (refl_equal true).

What has changed?

proux01 commented 2 years ago

Any idea what "before" means? I tested down to mathcomp 1.8.0 and it still wasn't compiling.