Renommage hypothèses de nom redondant dans les environnements

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

2 files changed, 12 insertions, 2 deletions

diff --git a/kernel/sign.ml b/kernel/sign.ml
index 00a160ffd6..fb2c8d31d2 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -243,6 +243,14 @@ let lookup_id id env =
   with 
     | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y)
 
+let make_all_name_different (ENVIRON((dom,_) as sign,dbs)) =
+  let _,newdbs =
+    List.fold_right
+      (fun (na,t) (avoid,newdbs) -> 
+	 let id = next_name_away na avoid in
+	 (id::avoid),((Name id,t)::newdbs))
+      dbs (dom,[])
+  in ENVIRON (sign,newdbs)
 
 type 'b assumptions = (typed_type,'b) sign
 type context = (typed_type,typed_type) sign
diff --git a/kernel/sign.mli b/kernel/sign.mli
index f4f26994f9..763a674716 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -9,7 +9,7 @@ open Term
 
 (* Signatures of named variables. *)
 
-type 'a signature (* = [identifier list * 'a list] *)
+type 'a signature
 
 val nil_sign : 'a signature
 val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
@@ -63,7 +63,7 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term
 
 (*s Signatures with named and de Bruijn variables. *)
 
-type 'a db_signature (* = [ (name * 'a) list ] *)
+type 'a db_signature
 type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
 
 val gLOB : 'b signature -> ('b,'a) sign
@@ -90,6 +90,8 @@ val number_of_rels : ('b,'a) sign -> int
 (* raise [Not_found] if the integer is out of range *)
 val change_name_env: ('a, 'b) sign -> int -> identifier -> ('a, 'b) sign
 
+val make_all_name_different : ('a, 'b) sign -> ('a, 'b) sign
+
 type ('b,'a) search_result =
   | GLOBNAME of identifier  * 'b
   | RELNAME of int * 'a