From 5f8fa89034b5ef43a7f8de51782733bdb43cec3a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 24 Sep 2010 22:23:07 +0000
Subject: Fixed a bug in printing fix/cofix error messages when several
 instances of the same variable name occur.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13465 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 947817909a..6f1d0473a0 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -228,6 +228,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
       str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++
       str "which should be an inductive type"
   | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) ->
+      let arg_env = make_all_name_different arg_env in
       let called =
         match names.(j) with
             Name id -> pr_id id
@@ -288,6 +289,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
   pr_ne_context_of (str "In environment") env ++
   st ++ str "." ++ fnl () ++
   (try (* May fail with unresolved globals. *)
+      let fixenv = make_all_name_different fixenv in
       let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in
 	str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
     with _ -> mt ())
-- 
cgit v1.2.3