Removing the type class for number of robots.

This is to be discussed. Let us leave it as before for now.

Core/Identifiers.v

@@ -125,12 +125,10 @@ Qed.
 
 Section Robots.
 
-Context (n m : nat) {ln lm : nat} {ltc_l_n : ln <c n} {ltc_l_m : lm <c m}.
-
 (** Given a number of correct and Byzantine robots, we can build canonical names.
     It is not declared as a global instance to avoid creating spurious settings. *)
-Definition Robots : Names.
-Proof using n m.
+Definition Robots (n m : nat) : Names.
+Proof using .
   refine {|
     nG := n;
     nB := m;
@@ -149,37 +147,45 @@ Proof using n m.
   + intros ? ?. apply enum_eq.
   + intros ? ?. apply enum_eq.
 Defined.
+
 Global Opaque G B.
+(* TODO: discuss this
+Section NM.
 
-Notation G := (@G Robots).
-Notation B := (@B Robots).
+Variables n m: nat.
 
-Lemma G_Robots : G = fin n.
+Notation GRob := (@G (Robots n m)).
+Notation BRob := (@B (Robots n m)).
+
+Lemma GRob_Robots : GRob = fin n.
 Proof using . reflexivity. Qed.
 
-Lemma B_Robots : B = fin m.
+Lemma BRob_Robots : BRob = fin m.
 Proof using . reflexivity. Qed.
 
-Lemma G_Robots_eq_iff : ∀ g1 g2 : G, g1 = g2 :> G <-> g1 = g2 :> fin n.
+Lemma GRob_Robots_eq_iff : forall g1 g2 : GRob, g1 = g2 :> GRob <-> g1 = g2 :> fin n.
 Proof using . reflexivity. Qed.
 
-Lemma B_Robots_eq_iff : ∀ b1 b2 : B, b1 = b2 :> B <-> b1 = b2 :> fin m.
+Lemma BRob_Robots_eq_iff : forall b1 b2 : BRob, b1 = b2 :> BRob <-> b1 = b2 :> fin m.
 Proof using . reflexivity. Qed.
 
-Definition good0 : G := fin0.
+Definition good0 : GRob := fin0.
+
+Definition byz0 : BRob := fin0.
 
-Definition byz0 : B := fin0.
+Lemma all_good0 : forall g : GRob, n = 1 -> g = good0.
+Proof using . intros * H. rewrite GRob_Robots_eq_iff. apply all_fin0, H. Qed.
 
-Lemma all_good0 : ∀ g : G, n = 1 -> g = good0.
-Proof using . intros * H. rewrite G_Robots_eq_iff. apply all_fin0, H. Qed.
+Lemma all_good_eq : forall g1 g2 : GRob, n = 1 -> g1 = g2.
+Proof using ltc_l_n. intros * H. rewrite GRob_Robots_eq_iff. apply all_eq, H. Qed.
 
-Lemma all_good_eq : ∀ g1 g2 : G, n = 1 -> g1 = g2.
-Proof using ltc_l_n. intros * H. rewrite G_Robots_eq_iff. apply all_eq, H. Qed.
+Lemma all_byz0 : forall b : BRob, m = 1 -> b = byz0.
+Proof using . intros * H. rewrite BRob_Robots_eq_iff. apply all_fin0, H. Qed.
 
-Lemma all_byz0 : ∀ b : B, m = 1 -> b = byz0.
-Proof using . intros * H. rewrite B_Robots_eq_iff. apply all_fin0, H. Qed.
+Lemma all_byz_eq : forall b1 b2 : BRob, m = 1 -> b1 = b2.
+Proof using ltc_l_m. intros * H. rewrite BRob_Robots_eq_iff. apply all_eq, H. Qed.
+End NM.
 
-Lemma all_byz_eq : ∀ b1 b2 : B, m = 1 -> b1 = b2.
-Proof using ltc_l_m. intros * H. rewrite B_Robots_eq_iff. apply all_eq, H. Qed.
+*)
 
 End Robots.