From 74263802c2aa7398b31bf5ddfcccaaddb46a45e4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 May 2000 19:54:35 +0000
Subject: 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
---
 kernel/sign.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'kernel/sign.ml')

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
-- 
cgit v1.2.3