Modulification of identifier

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

3 files changed, 25 insertions, 25 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 2155171c9..f029c053a 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -98,7 +98,7 @@ type cinfo=
 type term=
     Symb of constr
   | Product of sorts_family * sorts_family
-  | Eps of identifier
+  | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
@@ -106,7 +106,7 @@ let rec term_equal t1 t2 =
   match t1, t2 with
     | Symb c1, Symb c2 -> eq_constr c1 c2
     | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2
-    | Eps i1, Eps i2 -> id_ord i1 i2 = 0
+    | Eps i1, Eps i2 -> Id.compare i1 i2 = 0
     | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
     | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1},
       Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} ->
@@ -149,7 +149,7 @@ type patt_kind =
   | Creates_variables
 
 type quant_eq =
-    {qe_hyp_id: identifier;
+    {qe_hyp_id: Id.t;
      qe_pol: bool;
      qe_nvars:int;
      qe_lhs: ccpattern;
@@ -203,7 +203,7 @@ module Termhash = Hashtbl.Make
    end)
 
 module Identhash = Hashtbl.Make
-  (struct type t = identifier
+  (struct type t = Id.t
 	  let equal = Pervasives.(=)
 	  let hash = Hashtbl.hash
    end)
@@ -356,8 +356,8 @@ let new_representative typ =
 
 (* rebuild a constr from an applicative term *)
 
-let _A_ = Name (id_of_string "A")
-let _B_ = Name (id_of_string "A")
+let _A_ = Name (Id.of_string "A")
+let _B_ = Name (Id.of_string "A")
 let _body_ =  mkProd(Anonymous,mkRel 2,mkRel 2)
 
 let cc_product s1 s2 =
@@ -722,7 +722,7 @@ let one_step state =
 	    true
 	with Not_found -> false
 
-let __eps__ = id_of_string "_eps_"
+let __eps__ = Id.of_string "_eps_"
 
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 6232b126e..5d286c732 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -18,7 +18,7 @@ type cinfo =
 type term =
     Symb of constr
   | Product of sorts_family * sorts_family
-  | Eps of identifier
+  | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
@@ -87,7 +87,7 @@ val add_equality : state -> constr -> term -> term -> unit
 
 val add_disequality : state -> from -> term -> term -> unit
 
-val add_quant : state -> identifier -> bool ->
+val add_quant : state -> Id.t -> bool ->
   int * patt_kind * ccpattern * patt_kind * ccpattern -> unit
 
 val tail_pac : pa_constructor -> pa_constructor
@@ -106,7 +106,7 @@ val join_path : forest -> int -> int ->
   ((int * int) * equality) list * ((int * int) * equality) list
 
 type quant_eq=
-    {qe_hyp_id: identifier;
+    {qe_hyp_id: Id.t;
      qe_pol: bool;
      qe_nvars:int;
      qe_lhs: ccpattern;
@@ -161,7 +161,7 @@ type term =
 
 type rule =
     Congruence
-  | Axiom of Names.identifier
+  | Axiom of Names.Id.t
   | Injection of int*int*int*int
 
 type equality =
@@ -207,19 +207,19 @@ val process_rec : UF.t -> equality list -> int list
 val cc : UF.t -> unit
 
 val make_uf :
-  (Names.identifier * (term * term)) list -> UF.t
+  (Names.Id.t * (term * term)) list -> UF.t
 
 val add_one_diseq : UF.t -> (term * term) -> int * int
 
 val add_disaxioms :
-  UF.t -> (Names.identifier * (term * term)) list ->
-  (Names.identifier * (int * int)) list
+  UF.t -> (Names.Id.t * (term * term)) list ->
+  (Names.Id.t * (int * int)) list
 
 val check_equal : UF.t -> int * int -> bool
 
 val find_contradiction : UF.t ->
-  (Names.identifier * (int * int)) list ->
-  (Names.identifier * (int * int))
+  (Names.Id.t * (int * int)) list ->
+  (Names.Id.t * (int * int))
 *)
 
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7d4d1728a..9a2f23d64 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -238,7 +238,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let pred=mkLambda(Anonymous,intype,outtype) in
   let case_info=make_case_info (pf_env gls) ind RegularStyle in
   let body= mkCase(case_info, pred, casee, branches) in
-  let id=pf_get_new_id (id_of_string "t") gls in
+  let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
@@ -275,7 +275,7 @@ let rec proof_tac p gls =
 	let typf = Termops.refresh_universes (pf_type_of gls tf1) in
 	let typx = Termops.refresh_universes (pf_type_of gls tx1) in
 	let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
-	let id = pf_get_new_id (id_of_string "f") gls in
+	let id = pf_get_new_id (Id.of_string "f") gls in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
 	  mkApp(Lazy.force _f_equal,
@@ -316,7 +316,7 @@ let refute_tac c t1 t2 p gls =
   let neweq=
     mkApp(Lazy.force _eq,
 	  [|intype;tt1;tt2|]) in
-  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let hid=pf_get_new_id (Id.of_string "Heq") gls in
   let false_t=mkApp (c,[|mkVar hid|]) in
     tclTHENS (assert_tac (Name hid) neweq)
       [proof_tac p; simplest_elim false_t] gls
@@ -325,8 +325,8 @@ let convert_to_goal_tac c t1 t2 p gls =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let sort = Termops.refresh_universes (pf_type_of gls tt2) in
   let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
-  let e=pf_get_new_id (id_of_string "e") gls in
-  let x=pf_get_new_id (id_of_string "X") gls in
+  let e=pf_get_new_id (Id.of_string "e") gls in
+  let x=pf_get_new_id (Id.of_string "X") gls in
   let identity=mkLambda (Name x,sort,mkRel 1) in
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
@@ -335,7 +335,7 @@ let convert_to_goal_tac c t1 t2 p gls =
 
 let convert_to_hyp_tac c1 t1 c2 t2 p gls =
   let tt2=constr_of_term t2 in
-  let h=pf_get_new_id (id_of_string "H") gls in
+  let h=pf_get_new_id (Id.of_string "H") gls in
   let false_t=mkApp (c2,[|mkVar h|]) in
     tclTHENS (assert_tac (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
@@ -346,13 +346,13 @@ let discriminate_tac cstr p gls =
   let intype = Termops.refresh_universes (pf_type_of gls t1) in
   let concl=pf_concl gls in
   let outsort = mkType (Termops.new_univ ()) in
-  let xid=pf_get_new_id (id_of_string "X") gls in
-  let tid=pf_get_new_id (id_of_string "t") gls in
+  let xid=pf_get_new_id (Id.of_string "X") gls in
+  let tid=pf_get_new_id (Id.of_string "t") gls in
   let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
   let trivial=pf_type_of gls identity in
   let outtype = mkType (Termops.new_univ ()) in
   let pred=mkLambda(Name xid,outtype,mkRel 1) in
-  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let hid=pf_get_new_id (Id.of_string "Heq") gls in
   let proj=build_projection intype outtype cstr trivial concl gls in
   let injt=mkApp (Lazy.force _f_equal,
 		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in