diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
| commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
| tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /interp/constrextern.ml | |
| parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) | |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b2b21925..fd230539 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: constrextern.ml 13492 2010-10-04 21:20:01Z herbelin $ *) (*i*) open Pp @@ -602,7 +602,7 @@ let rec extern inctx scopes vars r = extern_symbol scopes vars r'' (uninterp_notations r'') with No_match -> match r' with | RRef (loc,ref) -> - extern_global loc (implicits_of_global ref) + extern_global loc (select_stronger_impargs (implicits_of_global ref)) (extern_reference loc vars ref) | RVar (loc,id) -> CRef (Ident (loc,id)) @@ -655,7 +655,8 @@ let rec extern inctx scopes vars r = CRecord (loc, None, List.rev (ip projs locals args [])) with | Not_found | No_match | Exit -> - extern_app loc inctx (implicits_of_global ref) + extern_app loc inctx + (select_stronger_impargs (implicits_of_global ref)) (Some ref,extern_reference rloc vars ref) args end | _ -> @@ -828,12 +829,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function let subscopes = try list_skipn n (find_arguments_scope ref) with _ -> [] in let impls = - try list_skipn n (implicits_of_global ref) with _ -> [] in + let impls = + select_impargs_size + (List.length args) (implicits_of_global ref) in + try list_skipn n impls with _ -> [] in (if n = 0 then f else RApp (dummy_loc,f,args1)), args2, subscopes, impls | RApp (_,(RRef (_,ref) as f),args), None -> let subscopes = find_arguments_scope ref in - let impls = implicits_of_global ref in + let impls = + select_impargs_size + (List.length args) (implicits_of_global ref) in f, args, subscopes, impls | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], [] | _, None -> t, [], [], [] |