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

3 files changed, 17 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
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 2dfd35a0e7..644616dd26 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -21,6 +21,7 @@ open Ast
 let guill s = "\""^s^"\""
 
 let explain_unbound_rel k ctx n =
+  let ctx = make_all_name_different ctx in
   let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
   [< 'sTR"Unbound reference: "; pe; 'fNL;
      'sTR"The reference "; 'iNT n; 'sTR" is free" >]
@@ -30,6 +31,7 @@ let explain_cant_execute k ctx c =
   [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >]
 
 let explain_not_type k ctx c =
+  let ctx = make_all_name_different ctx in
   let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
   let pc = prterm_env ctx c in
   [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
@@ -93,6 +95,7 @@ let explain_ill_formed_branch k ctx c i actty expty =
      'sTR "which should be"; 'bRK(1,1); pe >]
 
 let explain_generalization k ctx (name,var) c =
+  let ctx = make_all_name_different ctx in
   let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
   let pv = prterm_env ctx (body_of_type var) in
   let pc = prterm_env (add_rel (name,var) ctx) c in
@@ -102,6 +105,7 @@ let explain_generalization k ctx (name,var) c =
      'sTR"which should be typed by Set, Prop or Type." >]
 
 let explain_actual_type k ctx c ct pt =
+  let ctx = make_all_name_different ctx in
   let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
   let pc = prterm_env ctx c in
   let pct = prterm_env ctx ct in
@@ -112,6 +116,7 @@ let explain_actual_type k ctx c ct pt =
      'sTR"Actually, it has type" ; 'bRK(1,1); pct >]
 
 let explain_cant_apply k ctx s rator randl =
+  let ctx = make_all_name_different ctx in
   let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
   let pr = prterm_env ctx rator.uj_val in
   let prt = prterm_env ctx rator.uj_type in