1 files changed, 5 insertions, 9 deletions
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index 65083791ca..37eef12381 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -90,15 +90,15 @@ Class PropUOp (Op : Prop -> Prop) :=
     NB1: The Ltac code is currently limited to (Op: Z -> Z -> Z)
     NB2: This is not sufficient to cope with [Z.div] or [Z.mod]
  *)
-Class BinOpSpec {S T: Type} (Op : T -> T -> T) {I : InjTyp S T} :=
+Class BinOpSpec {T1 T2 T3: Type} (Op : T1 -> T2 -> T3)  :=
   mkbspec {
-      BPred : T -> T -> T -> Prop;
+      BPred : T1 -> T2 -> T3 -> Prop;
       BSpec : forall x y, BPred x y (Op x y)
     }.
 
-Class UnOpSpec {S T: Type} (Op : T -> T) {I : InjTyp S T} :=
+Class UnOpSpec {T1 T2: Type} (Op : T1 -> T2)  :=
   mkuspec {
-      UPred : T -> T -> Prop;
+      UPred : T1 -> T2 -> Prop;
       USpec : forall x, UPred x (Op x)
     }.
 
@@ -220,8 +220,6 @@ Proof.
   exact (fun H => proj1 IFF H).
 Qed.
 
-Definition identity (A : Type) : A -> A := fun x => x.
-
 (** Registering constants for use by the plugin *)
 Register eq_iff      as ZifyClasses.eq_iff.
 Register target_prop as ZifyClasses.target_prop.
@@ -265,6 +263,4 @@ Register iff_morph as ZifyClasses.iff_morph.
 Register impl_morph as ZifyClasses.impl_morph.
 Register not as ZifyClasses.not.
 Register not_morph as ZifyClasses.not_morph.
-
-(** Identify function *)
-Register identity as ZifyClasses.identity.
+Register True as ZifyClasses.True.