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/generic_quotient.v | |
| parent | 79aa2b1ab5b233f103cd3e402094cd93d9028866 (diff) | |
Remove pack constructors
Diffstat (limited to 'mathcomp/ssreflect/generic_quotient.v')
| -rw-r--r-- | mathcomp/ssreflect/generic_quotient.v | 4 |
1 files changed, 1 insertions, 3 deletions
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. |