Modulification of name

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

12 files changed, 76 insertions, 76 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 966ebff40..5b7f0b4c7 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -11,7 +11,7 @@ open Pp
 open Tacexpr
 
 type 'it statement =
-    {st_label:name;
+    {st_label:Name.t;
      st_it:'it}
 
 type thesis_kind =
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index fb7e5c29a..107b65366 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -28,10 +28,10 @@ val proof_instr: Decl_expr.raw_proof_instr -> unit
 val tcl_change_info : Decl_mode.pm_info -> tactic
 
 val execute_cases :
-    Names.name ->
+    Name.t ->
     Decl_mode.per_info ->
     (Term.constr -> Proof_type.tactic) ->
-    (Names.Id.Set.elt * (Term.constr option * Term.constr list) list) list ->
+    (Id.Set.elt * (Term.constr option * Term.constr list) list) list ->
     Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
 
 val tree_of_pats : 
@@ -44,8 +44,8 @@ val add_branch :
 
 val append_branch :
   Id.t *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
-  (Names.Id.Set.t * Decl_mode.split_tree) option ->
-  (Names.Id.Set.t * Decl_mode.split_tree) option
+  (Id.Set.t * Decl_mode.split_tree) option ->
+  (Id.Set.t * Decl_mode.split_tree) option
 
 val append_tree :
   Id.t * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
@@ -58,7 +58,7 @@ val build_dep_clause :   Term.types Decl_expr.statement list ->
     Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
 
 val register_dep_subcase :    
-    Names.Id.t * (int * int) ->
+    Id.t * (int * int) ->
     Environ.env ->
     Decl_mode.per_info ->
     Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
@@ -69,41 +69,41 @@ val thesis_for :     Term.constr ->
 val close_previous_case : Proof.proof -> unit
 
 val pop_stacks :
-  (Names.Id.t *
+  (Id.t *
      (Term.constr option * Term.constr list) list) list ->
-  (Names.Id.t *
+  (Id.t *
      (Term.constr option * Term.constr list) list) list
 
 val push_head :   Term.constr ->
-  Names.Id.Set.t ->
-  (Names.Id.t *
+  Id.Set.t ->
+  (Id.t *
      (Term.constr option * Term.constr list) list) list ->
-  (Names.Id.t *
+  (Id.t *
      (Term.constr option * Term.constr list) list) list
 
 val push_arg : Term.constr ->
-  (Names.Id.t *
+  (Id.t *
      (Term.constr option * Term.constr list) list) list ->
-  (Names.Id.t *
+  (Id.t *
      (Term.constr option * Term.constr list) list) list
 
 val hrec_for:
-    Names.Id.t ->
+    Id.t ->
     Decl_mode.per_info -> Proof_type.goal Tacmach.sigma ->
-    Names.Id.t -> Term.constr
+    Id.t -> Term.constr
 
 val consider_match :
    bool ->
-    (Names.Id.Set.elt*bool) list ->
-    Names.Id.Set.elt list ->
+    (Id.Set.elt*bool) list ->
+    Id.Set.elt list ->
     (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list ->
     Proof_type.tactic
 
 val init_tree:
-    Names.Id.Set.t ->
-    Names.inductive ->
+    Id.Set.t ->
+    inductive ->
     int option * Declarations.wf_paths ->
     (int ->
      (int option * Declarations.recarg Rtree.t) array ->
-     (Names.Id.Set.t * Decl_mode.split_tree) option) ->
+     (Id.Set.t * Decl_mode.split_tree) option) ->
     Decl_mode.split_tree
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 1c70908b6..bd8d549a2 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -79,7 +79,7 @@ val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast
 
 val anonymous_name : Id.t
 val dummy_name : Id.t
-val id_of_name : name -> Id.t
+val id_of_name : Name.t -> Id.t
 val id_of_mlid : ml_ident -> Id.t
 val tmp_id : ml_ident -> ml_ident
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index b69715fc9..1a97689b5 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -38,7 +38,7 @@ val error_MPfile_as_mod : module_path -> bool -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit
-val msg_non_implicit : global_reference -> int -> name -> string
+val msg_non_implicit : global_reference -> int -> Name.t -> string
 val error_non_implicit : string -> 'a
 
 val info_file : string -> unit
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9678fb547..f549adf7a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -169,7 +169,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     begin
       try
 	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
-	let new_x : name = get_name (Termops.ids_of_context env) x in
+	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (x,None,t) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	 if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
@@ -198,7 +198,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       try
 	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
 	let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
-	let new_x : name = get_name (Termops.ids_of_context env) x in
+	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (x,Some v,t) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index cf7d8e8fe..8acd24c88 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -22,9 +22,9 @@ let observe strm =
 
 
 type binder_type =
-  | Lambda of name
-  | Prod of name
-  | LetIn of name
+  | Lambda of Name.t
+  | Prod of Name.t
+  | LetIn of Name.t
 
 type glob_context = (binder_type*glob_constr) list
 
@@ -138,7 +138,7 @@ let apply_args ctxt body args =
   let need_convert avoid  bt =
     List.exists (need_convert_id avoid) (ids_of_binder bt)
   in
-  let next_name_away (na:name) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
+  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
     match na with
        | Name id when List.mem id avoid ->
 	   let new_id = Namegen.next_ident_away id avoid in
@@ -1186,7 +1186,7 @@ and compute_cst_params_from_app acc (params,rtl) =
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
-let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts =
+let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts =
   let rels_params =
     Array.mapi
       (fun i args ->
@@ -1222,13 +1222,13 @@ let rec rebuild_return_type rt =
 	Constrexpr.CProdN(loc,n,rebuild_return_type t')
     | Constrexpr.CLetIn(loc,na,t,t') ->
 	Constrexpr.CLetIn(loc,na,t,rebuild_return_type t')
-    | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Names.Anonymous],
+    | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous],
 				       Constrexpr.Default Decl_kinds.Explicit,rt],
 			    Constrexpr.CSort(Loc.ghost,GType None))
 
 
 let do_build_inductive
-    funnames (funsargs: (Names.name * glob_constr * bool) list list)
+    funnames (funsargs: (Name.t * glob_constr * bool) list list)
     returned_types
     (rtl:glob_constr list) =
   let _time1 = System.get_time () in
@@ -1257,7 +1257,7 @@ let do_build_inductive
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
     let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-      let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list  =
+      let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
 	funargs
       in
       List.fold_right
@@ -1323,7 +1323,7 @@ let do_build_inductive
     rel_constructors
   in
   let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-    let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list  =
+    let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
       (snd (List.chop nrel_params funargs))
     in
     List.fold_right
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 87fcb1022..101be24fd 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -1,5 +1,4 @@
-
-
+open Names
 
 (*
   [build_inductive parametrize funnames funargs returned_types bodies]
@@ -8,8 +7,8 @@
 *)
 
 val build_inductive :
-  Names.Id.t list -> (* The list of function name *)
-  (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
+  Id.t list -> (* The list of function name *)
+  (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
   unit
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 55d793e03..0f10636f0 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,8 +1,9 @@
+open Names
 open Glob_term
 open Misctypes
 
 (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
-val get_pattern_id : cases_pattern -> Names.Id.t list
+val get_pattern_id : cases_pattern -> Id.t list
 
 (* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
    [pat] must not contain occurences of anonymous pattern
@@ -14,11 +15,11 @@ val pattern_to_term : cases_pattern -> glob_constr
    In each of them the location is Util.Loc.ghost
 *)
 val mkGRef : Globnames.global_reference -> glob_constr
-val mkGVar : Names.Id.t -> glob_constr
+val mkGVar : Id.t -> glob_constr
 val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
-val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr
-val mkGProd : Names.name * glob_constr * glob_constr -> glob_constr
-val mkGLetIn : Names.name * glob_constr * glob_constr -> glob_constr
+val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr
+val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr
+val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr
 val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
 val mkGSort : glob_sort -> glob_constr
 val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
@@ -27,15 +28,15 @@ val mkGCast : glob_constr* glob_constr -> glob_constr
   Some basic functions to decompose glob_constrs
   These are analogous to the ones constrs
 *)
-val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr
+val glob_decompose_prod : glob_constr -> (Name.t*glob_constr) list * glob_constr
 val glob_decompose_prod_or_letin :
-  glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr
-val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr
+  glob_constr -> (Name.t*glob_constr option*glob_constr option) list * glob_constr
+val glob_decompose_prod_n : int -> glob_constr -> (Name.t*glob_constr) list * glob_constr
 val glob_decompose_prod_or_letin_n : int -> glob_constr ->
-  (Names.name*glob_constr option*glob_constr option) list * glob_constr
-val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list  ->  glob_constr
+  (Name.t*glob_constr option*glob_constr option) list * glob_constr
+val glob_compose_prod : glob_constr -> (Name.t*glob_constr) list  ->  glob_constr
 val glob_compose_prod_or_letin: glob_constr ->
-  (Names.name*glob_constr option*glob_constr option) list  ->  glob_constr
+  (Name.t*glob_constr option*glob_constr option) list  ->  glob_constr
 val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list)
 
 
@@ -57,7 +58,7 @@ val  glob_make_or_list : glob_constr list -> glob_constr
 
 
 (* Replace the var mapped in the glob_constr/context *)
-val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr
+val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr
 
 
 
@@ -69,27 +70,27 @@ val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr
    [avoid] with the variables appearing in the result.
 *)
   val alpha_pat :
-    Names.Id.Map.key list ->
+    Id.Map.key list ->
     Glob_term.cases_pattern ->
-    Glob_term.cases_pattern * Names.Id.Map.key list *
-      Names.Id.t Names.Id.Map.t
+    Glob_term.cases_pattern * Id.Map.key list *
+      Id.t Id.Map.t
 
 (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
    conventions and  does not share bound variables with avoid
 *)
-val alpha_rt : Names.Id.t list -> glob_constr -> glob_constr
+val alpha_rt : Id.t list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
-val alpha_br : Names.Id.t list ->
-    Loc.t * Names.Id.t list * Glob_term.cases_pattern list *
+val alpha_br : Id.t list ->
+    Loc.t * Id.t list * Glob_term.cases_pattern list *
     Glob_term.glob_constr ->
-    Loc.t * Names.Id.t list * Glob_term.cases_pattern list *
+    Loc.t * Id.t list * Glob_term.cases_pattern list *
     Glob_term.glob_constr
 
 
 (* Reduction function *)
 val replace_var_by_term  :
-  Names.Id.t ->
+  Id.t ->
   Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
 
 
@@ -97,7 +98,7 @@ val replace_var_by_term  :
 (*
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
-val is_free_in : Names.Id.t -> glob_constr -> bool
+val is_free_in : Id.t -> glob_constr -> bool
 
 
 val are_unifiable : cases_pattern -> cases_pattern -> bool
@@ -109,10 +110,10 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
    ids_of_pat : cases_pattern -> Id.Set.t
    returns the set of variables appearing in a pattern
 *)
-val   ids_of_pat : cases_pattern -> Names.Id.Set.t
+val   ids_of_pat : cases_pattern -> Id.Set.t
 
 (* TODO: finish this function (Fix not treated) *)
-val ids_of_glob_constr: glob_constr -> Names.Id.Set.t
+val ids_of_glob_constr: glob_constr -> Id.Set.t
 
 (*
    removing let_in construction in a glob_constr
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 7d0f5a00e..d9f0f51ce 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -16,12 +16,12 @@ val msgnl : std_ppcmds -> unit
 val invalid_argument : string -> 'a
 
 val fresh_id : Id.t list -> string -> Id.t
-val fresh_name : Id.t list -> string -> name
-val get_name : Id.t list -> ?default:string -> name -> name
+val fresh_name : Id.t list -> string -> Name.t
+val get_name : Id.t list -> ?default:string -> Name.t -> Name.t
 
 val array_get_start : 'a array -> 'a array
 
-val id_of_name : name -> Id.t
+val id_of_name : Name.t -> Id.t
 
 val locate_ind : Libnames.reference -> inductive
 val locate_constant : Libnames.reference -> constant
@@ -36,10 +36,10 @@ val list_add_set_eq :
   ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
 
 val chop_rlambda_n : int -> Glob_term.glob_constr ->
-  (name*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
+  (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
 
 val chop_rprod_n : int -> Glob_term.glob_constr ->
-  (name*Glob_term.glob_constr) list * Glob_term.glob_constr
+  (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
 
 val def_of_const : Term.constr -> Term.constr
 val eq : Term.constr Lazy.t
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 089493079..30c60b52b 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -543,8 +543,8 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
    calls of branch 1 with all rec calls of branch 2. *)
 (* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
 let rec merge_rec_hyps shift accrec
-    (ltyp:(Names.name * glob_constr option * glob_constr option) list)
-    filter_shift_stable : (Names.name * glob_constr option * glob_constr option) list =
+    (ltyp:(Name.t * glob_constr option * glob_constr option) list)
+    filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list =
   let mergeonehyp t reldecl =
     match reldecl with
       | (nme,x,Some (GApp(_,i,args) as ind))
@@ -560,7 +560,7 @@ let rec merge_rec_hyps shift accrec
     | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
 
 
-let build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift =
+let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift =
   List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
 
 
@@ -584,9 +584,9 @@ let prnt_prod_or_letin nm letbdy typ =
 
 
 let rec merge_types shift accrec1
-    (ltyp1:(name * glob_constr option * glob_constr option) list)
-    (concl1:glob_constr) (ltyp2:(name * glob_constr option * glob_constr option) list) concl2
-    : (name * glob_constr option * glob_constr option) list * glob_constr =
+    (ltyp1:(Name.t * glob_constr option * glob_constr option) list)
+    (concl1:glob_constr) (ltyp2:(Name.t * glob_constr option * glob_constr option) list) concl2
+    : (Name.t * glob_constr option * glob_constr option) list * glob_constr =
   let _ = prstr "MERGE_TYPES\n" in
   let _ = prstr "ltyp 1 : " in
   let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7b77afd07..e662cd41d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -353,8 +353,8 @@ type ('a,'b) journey_info_tac =
 (* journey_info : specifies the actions to do on the different term constructors during the travelling of the term
 *)
 type journey_info = 
-    { letiN : ((name*constr*types*constr),constr) journey_info_tac;
-      lambdA : ((name*types*constr),constr) journey_info_tac;
+    { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac;
+      lambdA : ((Name.t*types*constr),constr) journey_info_tac;
       casE : ((constr infos -> tactic) -> constr infos -> tactic) -> 
 	((case_info * constr * constr * constr array),constr) journey_info_tac;
       otherS : (unit,constr) journey_info_tac;
diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml
index 3e2c8ade7..da7e57766 100644
--- a/plugins/xml/acic.ml
+++ b/plugins/xml/acic.ml
@@ -68,9 +68,9 @@ type aconstr =
   | AEvar      of id * existential_key * aconstr list
   | ASort      of id * sorts
   | ACast      of id * aconstr * aconstr
-  | AProds     of (id * name * aconstr) list * aconstr
-  | ALambdas   of (id * name * aconstr) list * aconstr
-  | ALetIns    of (id * name * aconstr) list * aconstr
+  | AProds     of (id * Name.t * aconstr) list * aconstr
+  | ALambdas   of (id * Name.t * aconstr) list * aconstr
+  | ALetIns    of (id * Name.t * aconstr) list * aconstr
   | AApp       of id * aconstr list
   | AConst     of id * explicit_named_substitution * uri
   | AInd       of id * explicit_named_substitution * uri * int