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, 5 insertions, 0 deletions

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