diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-06 18:04:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-06 18:04:12 +0000 |
| commit | 8bb0d9d3853cdbde4992be9cbde393f19edcdcbf (patch) | |
| tree | 4be870a5b7002df38e3d3d79564552cbd90af1f5 /interp | |
| parent | 1be34dd7aed0548fdff34e09416977134781b886 (diff) | |
Apply implicit types to local binders too
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6017 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 9217400bc..22251aabb 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -894,8 +894,10 @@ let internalise sigma env allow_soapp lvar c = intern (ids,Some Symbols.type_scope,scopes) and intern_local_binder ((ids,ts,sc as env),bl) = function - LocalRawAssum(nal,ty) -> - let ty = intern_type env ty in + | LocalRawAssum(nal,ty) -> + let (loc,na) = List.hd nal in + (* TODO: fail if several names with different implicit types *) + let ty = locate_if_isevar loc na (intern_type env ty) in List.fold_left (fun ((ids,ts,sc),bl) (_,na) -> ((name_fold Idset.add na ids,ts,sc), (na,None,ty)::bl)) |