From 43bcf0d5824cc7757fc473e15851cd483736afe6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 17 Oct 2004 08:59:49 +0000
Subject: Semble raisonnable de distinguer les noms aussi dans cant_apply

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6227 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/himsg.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8b1745bd3a..19fb70deb6 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -157,6 +157,7 @@ let explain_actual_type ctx j pt =
   str "while it is expected to have type" ++ brk(1,1) ++ pt
 
 let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
+  let ctx = make_all_name_different ctx in
   let randl = Array.to_list randl in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr,prt = prjudge_env ctx rator in
@@ -179,6 +180,7 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
   str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp
 
 let explain_cant_apply_not_functional ctx rator randl =
+  let ctx = make_all_name_different ctx in
   let randl = Array.to_list randl in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr = prterm_env ctx rator.uj_val in
-- 
cgit v1.2.3