Merge pull request #249 from anton-trunov/prenex-implicits

Merge Arguments and Prenex Implicits

1 files changed, 15 insertions, 17 deletions

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 76b0521..4487ab4 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -171,7 +171,7 @@ Proof. by []. Qed.
 
 Lemma eqP T : Equality.axiom (@eq_op T).
 Proof. by case: T => ? []. Qed.
-Arguments eqP [T x y].
+Arguments eqP {T x y}.
 
 Delimit Scope eq_scope with EQ.
 Open Scope eq_scope.
@@ -254,8 +254,8 @@ Proof. by rewrite eq_sym; apply: ifN. Qed.
 
 End Contrapositives.
 
-Arguments memPn [T1 A x].
-Arguments memPnC [T1 A x].
+Arguments memPn {T1 A x}.
+Arguments memPnC {T1 A x}.
 
 Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2.
 Proof.
@@ -363,10 +363,10 @@ Proof. by case: eqP; [left | right]. Qed.
 
 End EqPred.
 
-Arguments predU1P [T x y b].
-Arguments pred2P [T T2 x y z u].
-Arguments predD1P [T x y b].
-Prenex Implicits pred1 pred2 pred3 pred4 predU1 predC1 predD1 predU1P.
+Arguments predU1P {T x y b}.
+Arguments pred2P {T T2 x y z u}.
+Arguments predD1P {T x y b}.
+Prenex Implicits pred1 pred2 pred3 pred4 predU1 predC1 predD1.
 
 Notation "[ 'predU1' x & A ]" := (predU1 x [mem A])
   (at level 0, format "[ 'predU1'  x  &  A ]") : fun_scope.
@@ -597,14 +597,14 @@ Qed.
 End SubType.
 
 Arguments SubType [T P].
-Arguments Sub [T P s].
-Arguments vrefl [T P].
-Arguments vrefl_rect [T P].
+Arguments Sub {T P s}.
+Arguments vrefl {T P}.
+Arguments vrefl_rect {T P}.
 Arguments clone_subType [T P] U v [sT] _ [c Urec cK].
-Arguments insub [T P sT].
+Arguments insub {T P sT}.
 Arguments insubT [T] P [sT x].
-Arguments val_inj [T P sT].
-Prenex Implicits val Sub vrefl vrefl_rect insub insubd val_inj.
+Arguments val_inj {T P sT}.
+Prenex Implicits val insubd.
 
 Local Notation inlined_sub_rect :=
   (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px).
@@ -646,8 +646,7 @@ Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl)
  (at level 0, format "[ 'newType'  'for'  v  'by'  rec ]") : form_scope.
 
 Definition innew T nT x := @Sub T predT nT x (erefl true).
-Arguments innew [T nT].
-Prenex Implicits innew.
+Arguments innew {T nT}.
 
 Lemma innew_val T nT : cancel val (@innew T nT).
 Proof. by move=> u; apply: val_inj; apply: SubK. Qed.
@@ -737,8 +736,7 @@ Proof. by []. Qed.
 
 End SubEqType.
 
-Arguments val_eqP [T P sT x y].
-Prenex Implicits val_eqP.
+Arguments val_eqP {T P sT x y}.
 
 Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
   (at level 0, format "[ 'eqMixin'  'of'  T  'by'  <: ]") : form_scope.