From 09db4999b6fd09dd33ccdd423f72b86d1eb9fe86 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Sep 2009 08:29:07 +0000
Subject: Fixed error message "cannot infer the type of id" in presence of
 notations for binders (the name of the notation was mistakenly taken). This
 happened e.g. when using Utf8.v.

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

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e49f219af3..c251ffb24f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -240,6 +240,11 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
             (if lassoc then List.rev l else l) termin
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
+  | AHole (Evd.BinderType (Name id as na)) ->
+      let na =
+        try snd (coerce_to_name (fst (List.assoc id subst)))
+        with Not_found -> na in
+      RHole (loc,Evd.BinderType na)
   | t ->
       rawconstr_of_aconstr_with_binders loc (traverse_binder sub)
       (subst_aconstr_in_rawconstr loc interp sub) subinfos t
-- 
cgit v1.2.3