diff options
Diffstat (limited to 'mathcomp/ssreflect/eqtype.v')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index a5e8784..6ed4b97 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -132,8 +132,7 @@ Variables (T : Type) (cT : type). Definition class := let: Pack _ c := cT return class_of cT in c. -Definition pack c := @Pack T c. -Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c. +Definition clone := fun c & cT -> T & phant_id (@Pack T c) cT => Pack c. End ClassDef. @@ -141,7 +140,7 @@ Module Exports. Coercion sort : type >-> Sortclass. Notation eqType := type. Notation EqMixin := Mixin. -Notation EqType T m := (@pack T m). +Notation EqType T m := (@Pack T m). Notation "[ 'eqMixin' 'of' T ]" := (class _ : mixin_of T) (at level 0, format "[ 'eqMixin' 'of' T ]") : form_scope. Notation "[ 'eqType' 'of' T 'for' C ]" := (@clone T C _ idfun id) |