Modulification of name

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

1 files changed, 24 insertions, 23 deletions

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