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

1 files changed, 8 insertions, 0 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