diff options
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/generic_quotient.v | 4 |
2 files changed, 3 insertions, 6 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) diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index ea929d7..f30c3a1 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -131,8 +131,6 @@ Record quotType := QuotTypePack { quot_class : quot_class_of quot_sort }. -Definition QuotType_pack qT m := @QuotTypePack qT m. - Variable qT : quotType. Definition pi_phant of phant qT := quot_pi (quot_class qT). Local Notation "\pi" := (pi_phant (Phant qT)). @@ -193,7 +191,7 @@ Canonical pi_unlock := Unlockable Pi.E. Canonical repr_unlock := Unlockable Repr.E. Notation quot_class_of := quot_mixin_of. -Notation QuotType Q m := (@QuotType_pack _ Q m). +Notation QuotType Q m := (@QuotTypePack _ Q m). Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id) (at level 0, format "[ 'quotType' 'of' Q ]") : form_scope. |