diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6316228e71..c651d11cba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -39,7 +39,7 @@ type var_internalization_data = in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) identifier list * (* signature of impargs of the variable *) - Impargs.implicits_list * + Impargs.implicit_status list * (* subscopes of the args of the variable *) scope_name option list @@ -555,7 +555,7 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference loc "<>" (string_of_id id) tys; - RVar (loc,id), impls, argsc, expl_impls + RVar (loc,id), make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Idset.mem id ids or List.mem id ltacvars @@ -596,7 +596,7 @@ let find_appl_head_data = function | RApp (_,RRef (_,ref),l) as x when l <> [] & Flags.version_strictly_greater Flags.V8_2 -> let n = List.length l in - x,list_skipn_at_least n (implicits_of_global ref), + x,List.map (drop_first_implicits n) (implicits_of_global ref), list_skipn_at_least n (find_arguments_scope ref),[] | x -> x,[],[],[] @@ -1371,6 +1371,7 @@ let internalize sigma globalenv env allow_patvar lvar c = it_mkRLambda ibind body and intern_impargs c env l subscopes args = + let l = select_impargs_size (List.length args) l in let eargs, rargs = extract_explicit_arg l args in let rec aux n impl subscopes eargs rargs = let (enva,subscopes') = apply_scope_env env subscopes in |