diff options
| author | Anton Trunov | 2018-11-23 10:16:12 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-12-04 14:25:53 +0100 |
| commit | efbcb84f3ddfea53b7b914284d8fa80fdb7a56fd (patch) | |
| tree | 6c60e0b59dcf16b096ad284ea09f3e888a9833d2 /mathcomp/ssreflect/eqtype.v | |
| parent | 79aa2b1ab5b233f103cd3e402094cd93d9028866 (diff) | |
Remove pack constructors
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) |