reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / OrderedType.Lt,Eq,Gt

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 88 insertions, 88 deletions

diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 32cacf4c0..36cdb9775 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -229,7 +229,7 @@ Module Type Sord.
   Axiom lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
   Axiom lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
 
-  Definition cmp e e' := match Data.compare e e' with Eq _ => true | _ => false end.	
+  Definition cmp e e' := match Data.compare e e' with EQ _ => true | _ => false end.	
 
   Parameter eq_1 : forall m m', Equal cmp m m' -> eq m m'.
   Parameter eq_2 : forall m m', eq m m' -> Equal cmp m m'.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 43b3045ce..ae52ce6b7 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -101,9 +101,9 @@ Fixpoint mem (k : key) (s : t elt) {struct s} : bool :=
   | nil => false
   | (k',_) :: l =>
      match X.compare k k' with
-      | Lt _ => false
-      | Eq _ => true
-      | Gt _ => mem k l
+      | LT _ => false
+      | EQ _ => true
+      | GT _ => mem k l
      end
  end.
 
@@ -141,9 +141,9 @@ Fixpoint find (k:key) (s: t elt) {struct s} : option elt :=
   | nil => None
   | (k',x)::s' => 
      match X.compare k k' with
-      | Lt _ => None
-      | Eq _ => Some x
-      | Gt _ => find k s'
+      | LT _ => None
+      | EQ _ => Some x
+      | GT _ => find k s'
      end
  end.
 
@@ -179,9 +179,9 @@ Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt :=
   | nil => (k,x) :: nil
   | (k',y) :: l =>
      match X.compare k k' with
-      | Lt _ => (k,x)::s
-      | Eq _ => (k,x)::l
-      | Gt _ => (k',y) :: add k x l
+      | LT _ => (k,x)::s
+      | EQ _ => (k,x)::l
+      | GT _ => (k',y) :: add k x l
      end
  end.
 
@@ -247,9 +247,9 @@ Fixpoint remove (k : key) (s : t elt) {struct s} : t elt :=
   | nil => nil
   | (k',x) :: l =>
      match X.compare k k' with
-      | Lt _ => s
-      | Eq _ => l
-      | Gt _ => (k',x) :: remove k l
+      | LT _ => s
+      | EQ _ => l
+      | GT _ => (k',x) :: remove k l
      end
  end.  
 
@@ -361,7 +361,7 @@ Fixpoint equal (cmp:elt->elt->bool)(m m' : t elt) { struct m } : bool :=
    | nil, nil => true
    | (x,e)::l, (x',e')::l' => 
       match X.compare x x' with 
-       | Eq _ => cmp e e' && equal cmp l l'
+       | EQ _ => cmp e e' && equal cmp l l'
        | _    => false
       end 
    | _, _ => false 
@@ -684,9 +684,9 @@ Fixpoint map2 (m : t elt) : t elt' -> t elt'' :=
          | nil => map2_l m
          | (k',e') :: l' =>
             match X.compare k k' with
-             | Lt _ => option_cons k (f (Some e) None) (map2 l m')
-             | Eq _ => option_cons k (f (Some e) (Some e')) (map2 l l')
-             | Gt _ => option_cons k' (f None (Some e')) (map2_aux l')
+             | LT _ => option_cons k (f (Some e) None) (map2 l m')
+             | EQ _ => option_cons k (f (Some e) (Some e')) (map2 l l')
+             | GT _ => option_cons k' (f None (Some e')) (map2_aux l')
             end
         end
   end.      
@@ -702,9 +702,9 @@ Fixpoint combine (m : t elt) : t elt' -> t oee' :=
          | nil => map (fun e => (Some e,None)) m
          | (k',e') :: l' =>
             match X.compare k k' with
-             | Lt _ => (k,(Some e, None))::combine l m'
-             | Eq _ => (k,(Some e, Some e'))::combine l l'
-             | Gt _ => (k',(None,Some e'))::combine_aux l'
+             | LT _ => (k,(Some e, None))::combine l m'
+             | EQ _ => (k,(Some e, Some e'))::combine l l'
+             | GT _ => (k',(None,Some e'))::combine_aux l'
             end
         end
   end. 
@@ -1099,14 +1099,14 @@ Import MD.
 
 Definition t := MapS.t D.t. 
 
-Definition cmp e e' := match D.compare e e' with Eq _ => true | _ => false end.
+Definition cmp e e' := match D.compare e e' with EQ _ => true | _ => false end.
 
 Fixpoint eq_list (m m' : list (X.t * D.t)) { struct m } : Prop := 
   match m, m' with 
    | nil, nil => True
    | (x,e)::l, (x',e')::l' => 
       match X.compare x x' with 
-       | Eq _ => D.eq e e' /\ eq_list l l'
+       | EQ _ => D.eq e e' /\ eq_list l l'
        | _       => False
       end 
    | _, _ => False
@@ -1121,9 +1121,9 @@ Fixpoint lt_list (m m' : list (X.t * D.t)) {struct m} : Prop :=
    | _, nil  => False
    | (x,e)::l, (x',e')::l' => 
       match X.compare x x' with 
-       | Lt _ => True
-       | Gt _ => False
-       | Eq _ => D.lt e e' \/ (D.eq e e' /\ lt_list l l')
+       | LT _ => True
+       | GT _ => False
+       | EQ _ => D.lt e e' \/ (D.eq e e' /\ lt_list l l')
       end
   end.
 
@@ -1254,18 +1254,18 @@ Definition compare : forall m1 m2, Compare lt eq m1 m2.
 Proof.
  intros (m1,Hm1); induction m1; 
  intros (m2, Hm2); destruct m2; 
-  [ apply Eq | apply Lt | apply Gt | ]; cmp_solve.
+  [ apply EQ | apply LT | apply GT | ]; cmp_solve.
  destruct a as (x,e); destruct p as (x',e'). 
  destruct (X.compare x x'); 
-  [ apply Lt | | apply Gt ]; cmp_solve.
+  [ apply LT | | apply GT ]; cmp_solve.
  destruct (D.compare e e'); 
-  [ apply Lt | | apply Gt ]; cmp_solve.
+  [ apply LT | | apply GT ]; cmp_solve.
  assert (Hm11 : sort (Raw.PX.ltk (elt:=D.t)) m1).
   inversion_clear Hm1; auto.
  assert (Hm22 : sort (Raw.PX.ltk (elt:=D.t)) m2).
   inversion_clear Hm2; auto.
  destruct (IHm1 Hm11 (Build_slist Hm22)); 
-  [ apply Lt | apply Eq | apply Gt ]; cmp_solve.
+  [ apply LT | apply EQ | apply GT ]; cmp_solve.
 Qed.
 
 End Make_ord. 
diff --git a/theories/FSets/FMap.v b/theories/FSets/FMaps.v
index dac1b4396..dac1b4396 100644
--- a/theories/FSets/FMap.v
+++ b/theories/FSets/FMaps.v
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 728aed9b3..5b2c08319 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -43,9 +43,9 @@ Module Raw (X: OrderedType).
     | nil => false
     | y :: l =>
         match X.compare x y with
-        | Lt _ => false
-        | Eq _ => true
-        | Gt _ => mem x l
+        | LT _ => false
+        | EQ _ => true
+        | GT _ => mem x l
         end
     end.
 
@@ -54,9 +54,9 @@ Module Raw (X: OrderedType).
     | nil => x :: nil
     | y :: l =>
         match X.compare x y with
-        | Lt _ => x :: s
-        | Eq _ => s
-        | Gt _ => y :: add x l
+        | LT _ => x :: s
+        | EQ _ => s
+        | GT _ => y :: add x l
         end
     end.
 
@@ -67,9 +67,9 @@ Module Raw (X: OrderedType).
     | nil => nil
     | y :: l =>
         match X.compare x y with
-        | Lt _ => s
-        | Eq _ => l
-        | Gt _ => y :: remove x l
+        | LT _ => s
+        | EQ _ => l
+        | GT _ => y :: remove x l
         end
     end.  
   
@@ -82,9 +82,9 @@ Module Raw (X: OrderedType).
            | nil => s
            | x' :: l' =>
                match X.compare x x' with
-               | Lt _ => x :: union l s'
-               | Eq _ => x :: union l l'
-               | Gt _ => x' :: union_aux l'
+               | LT _ => x :: union l s'
+               | EQ _ => x :: union l l'
+               | GT _ => x' :: union_aux l'
                end
            end)
     end.      
@@ -98,9 +98,9 @@ Module Raw (X: OrderedType).
            | nil => nil
            | x' :: l' =>
                match X.compare x x' with
-               | Lt _ => inter l s'
-               | Eq _ => x :: inter l l'
-               | Gt _ => inter_aux l'
+               | LT _ => inter l s'
+               | EQ _ => x :: inter l l'
+               | GT _ => inter_aux l'
                end
            end)
     end.  
@@ -114,9 +114,9 @@ Module Raw (X: OrderedType).
            | nil => s
            | x' :: l' =>
                match X.compare x x' with
-               | Lt _ => x :: diff l s'
-               | Eq _ => diff l l'
-               | Gt _ => diff_aux l'
+               | LT _ => x :: diff l s'
+               | EQ _ => diff l l'
+               | GT _ => diff_aux l'
                end
            end)
     end.  
@@ -127,7 +127,7 @@ Module Raw (X: OrderedType).
     | nil, nil => true
     | x :: l, x' :: l' =>
         match X.compare x x' with
-        | Eq _ => equal l l'
+        | EQ _ => equal l l'
         | _ => false
         end
     | _, _ => false
@@ -138,9 +138,9 @@ Module Raw (X: OrderedType).
     | nil, _ => true
     | x :: l, x' :: l' =>
         match X.compare x x' with
-        | Lt _ => false
-        | Eq _ => subset l l'
-        | Gt _ => subset s l'
+        | LT _ => false
+        | EQ _ => subset l l'
+        | GT _ => subset s l'
         end
     | _, _ => false
     end.
diff --git a/theories/FSets/FSet.v b/theories/FSets/FSets.v
index 51cd23c12..51cd23c12 100644
--- a/theories/FSets/FSet.v
+++ b/theories/FSets/FSets.v
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index ef8a1b8d7..cb31b388b 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -22,9 +22,9 @@ Unset Strict Implicit.
 (** * Ordered types *)
 
 Inductive Compare (X : Set) (lt eq : X -> X -> Prop) (x y : X) : Set :=
-  | Lt : lt x y -> Compare lt eq x y
-  | Eq : eq x y -> Compare lt eq x y
-  | Gt : lt y x -> Compare lt eq x y.
+  | LT : lt x y -> Compare lt eq x y
+  | EQ : eq x y -> Compare lt eq x y
+  | GT : lt y x -> Compare lt eq x y.
 
 Module Type OrderedType.
 
@@ -144,61 +144,61 @@ Ltac abstraction := match goal with
  | _ => idtac
 end.
 
-Ltac do_eq a b Eq := match goal with 
+Ltac do_eq a b EQ := match goal with 
  | |- lt ?x ?y -> _ => let H := fresh "H" in 
      (intro H; 
-      (generalize (eq_lt (eq_sym Eq) H); clear H; intro H) ||
-      (generalize (lt_eq H Eq); clear H; intro H) || 
+      (generalize (eq_lt (eq_sym EQ) H); clear H; intro H) ||
+      (generalize (lt_eq H EQ); clear H; intro H) || 
       idtac); 
-      do_eq a b Eq
+      do_eq a b EQ
  | |- ~lt ?x ?y -> _ => let H := fresh "H" in 
      (intro H; 
-      (generalize (eq_le (eq_sym Eq) H); clear H; intro H) ||
-      (generalize (le_eq H Eq); clear H; intro H) || 
+      (generalize (eq_le (eq_sym EQ) H); clear H; intro H) ||
+      (generalize (le_eq H EQ); clear H; intro H) || 
       idtac); 
-      do_eq a b Eq 
+      do_eq a b EQ 
  | |- eq ?x ?y -> _ => let H := fresh "H" in 
      (intro H; 
-      (generalize (eq_trans (eq_sym Eq) H); clear H; intro H) ||
-      (generalize (eq_trans H Eq); clear H; intro H) || 
+      (generalize (eq_trans (eq_sym EQ) H); clear H; intro H) ||
+      (generalize (eq_trans H EQ); clear H; intro H) || 
       idtac); 
-      do_eq a b Eq 
+      do_eq a b EQ 
  | |- ~eq ?x ?y -> _ => let H := fresh "H" in 
      (intro H; 
-      (generalize (eq_neq (eq_sym Eq) H); clear H; intro H) ||
-      (generalize (neq_eq H Eq); clear H; intro H) || 
+      (generalize (eq_neq (eq_sym EQ) H); clear H; intro H) ||
+      (generalize (neq_eq H EQ); clear H; intro H) || 
       idtac); 
-      do_eq a b Eq 
- | |- lt a ?y => apply eq_lt with b; [exact Eq|]
- | |- lt ?y a => apply lt_eq with b; [|exact (eq_sym Eq)]
- | |- eq a ?y => apply eq_trans with b; [exact Eq|]
- | |- eq ?y a => apply eq_trans with b; [|exact (eq_sym Eq)]
+      do_eq a b EQ 
+ | |- lt a ?y => apply eq_lt with b; [exact EQ|]
+ | |- lt ?y a => apply lt_eq with b; [|exact (eq_sym EQ)]
+ | |- eq a ?y => apply eq_trans with b; [exact EQ|]
+ | |- eq ?y a => apply eq_trans with b; [|exact (eq_sym EQ)]
  | _ => idtac
  end.
 
 Ltac propagate_eq := abstraction; clear; match goal with 
  (* the abstraction tactic leaves equality facts in head position...*)
  | |- eq ?a ?b -> _ => 
-     let Eq := fresh "Eq" in (intro Eq; do_eq a b Eq; clear Eq); 
+     let EQ := fresh "EQ" in (intro EQ; do_eq a b EQ; clear EQ); 
      propagate_eq 
  | _ => idtac
 end.
 
-Ltac do_lt x y Lt := match goal with 
- (* Lt *)
- | |- lt x y -> _ => intros _; do_lt x y Lt
+Ltac do_lt x y LT := match goal with 
+ (* LT *)
+ | |- lt x y -> _ => intros _; do_lt x y LT
  | |- lt y ?z -> _ => let H := fresh "H" in 
-     (intro H; generalize (lt_trans Lt H); intro); do_lt x y Lt
+     (intro H; generalize (lt_trans LT H); intro); do_lt x y LT
  | |- lt ?z x -> _ => let H := fresh "H" in 
-     (intro H; generalize (lt_trans H Lt); intro); do_lt x y Lt
- | |- lt _ _ -> _ => intro; do_lt x y Lt
+     (intro H; generalize (lt_trans H LT); intro); do_lt x y LT
+ | |- lt _ _ -> _ => intro; do_lt x y LT
  (* Ge *)
- | |- ~lt y x -> _ => intros _; do_lt x y Lt
+ | |- ~lt y x -> _ => intros _; do_lt x y LT
  | |- ~lt x ?z -> _ => let H := fresh "H" in 
-     (intro H; generalize (le_lt_trans H Lt); intro); do_lt x y Lt
+     (intro H; generalize (le_lt_trans H LT); intro); do_lt x y LT
  | |- ~lt ?z y -> _ => let H := fresh "H" in 
-     (intro H; generalize (lt_le_trans Lt H); intro); do_lt x y Lt
- | |- ~lt _ _ -> _ => intro; do_lt x y Lt
+     (intro H; generalize (lt_le_trans LT H); intro); do_lt x y LT
+ | |- ~lt _ _ -> _ => intro; do_lt x y LT
  | _ => idtac
  end.
 
@@ -207,8 +207,8 @@ Definition hide_lt := lt.
 Ltac propagate_lt := abstraction; match goal with 
  (* when no [=] remains, the abstraction tactic leaves [<] facts first. *)
  | |- lt ?x ?y -> _ => 
-     let Lt := fresh "Lt" in (intro Lt; do_lt x y Lt; 
-     change (hide_lt x y) in Lt); 
+     let LT := fresh "LT" in (intro LT; do_lt x y LT; 
+     change (hide_lt x y) in LT); 
      propagate_lt 
  | _ => unfold hide_lt in *
 end.
@@ -249,7 +249,7 @@ Ltac false_order := elimtype False; order.
 
   Lemma elim_compare_eq :
    forall x y : t,
-   eq x y -> exists H : eq x y, compare x y = Eq _ H.
+   eq x y -> exists H : eq x y, compare x y = EQ _ H.
   Proof. 
    intros; case (compare x y); intros H'; try solve [false_order].
    exists H'; auto.   
@@ -257,7 +257,7 @@ Ltac false_order := elimtype False; order.
 
   Lemma elim_compare_lt :
    forall x y : t,
-   lt x y -> exists H : lt x y, compare x y = Lt _ H.
+   lt x y -> exists H : lt x y, compare x y = LT _ H.
   Proof. 
    intros; case (compare x y); intros H'; try solve [false_order].
    exists H'; auto. 
@@ -265,7 +265,7 @@ Ltac false_order := elimtype False; order.
 
   Lemma elim_compare_gt :
    forall x y : t,
-   lt y x -> exists H : lt y x, compare x y = Gt _ H.
+   lt y x -> exists H : lt y x, compare x y = GT _ H.
   Proof. 
    intros; case (compare x y); intros H'; try solve [false_order].
    exists H'; auto.   
@@ -306,7 +306,7 @@ Ltac false_order := elimtype False; order.
   Definition eqb x y : bool := if eq_dec x y then true else false.
 
   Lemma eqb_alt : 
-    forall x y, eqb x y = match compare x y with Eq _ => true | _ => false end. 
+    forall x y, eqb x y = match compare x y with EQ _ => true | _ => false end. 
   Proof.
   unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto.
   Qed.