diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-27 08:29:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-27 08:29:07 +0000 |
| commit | 09db4999b6fd09dd33ccdd423f72b86d1eb9fe86 (patch) | |
| tree | 681722f782357413a7c2d65c303f0f056d7d52ab | |
| parent | f99dc2691ace6a691e7fd07e580e855e7bca7b55 (diff) | |
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
| -rw-r--r-- | interp/constrintern.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e49f219af..c251ffb24 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 |