From efbcb84f3ddfea53b7b914284d8fa80fdb7a56fd Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Fri, 23 Nov 2018 10:16:12 +0100
Subject: Remove pack constructors

---
 mathcomp/ssreflect/eqtype.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/eqtype.v')

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)
-- 
cgit v1.2.3