From 8bb0d9d3853cdbde4992be9cbde393f19edcdcbf Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 6 Aug 2004 18:04:12 +0000
Subject: 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
---
 interp/constrintern.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp')

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))
-- 
cgit v1.2.3