diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 16 | ||||
| -rw-r--r-- | interp/constrintern.ml | 10 | ||||
| -rw-r--r-- | interp/constrintern.mli | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 5 |
4 files changed, 22 insertions, 13 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, [], [], [] diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3bf556f1..d918e94d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: constrintern.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Util @@ -41,7 +41,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 @@ -557,7 +557,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 @@ -598,7 +598,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,[],[],[] @@ -815,6 +815,7 @@ let subst_cases_pattern loc alias intern fullsubst scopes a = match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v with Not_found -> anomaly "Inconsistent substitution of recursive notation") + | AHole _ -> ([],[[], PatVar (loc,Anonymous)]) | t -> error_invalid_pattern_notation loc in aux alias fullsubst a @@ -1372,6 +1373,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 diff --git a/interp/constrintern.mli b/interp/constrintern.mli index acb13a8b..02a51e7e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: constrintern.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: constrintern.mli 13492 2010-10-04 21:20:01Z herbelin $ i*) (*i*) open Names @@ -53,7 +53,7 @@ type var_internalization_data = identifier list * (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - Impargs.implicits_list * (* signature of impargs of the variable *) + Impargs.implicit_status list * (** signature of impargs of the variable *) scope_name option list (* subscopes of the args of the variable *) (* A map of free variables to their implicit arguments and scopes *) diff --git a/interp/notation.ml b/interp/notation.ml index fe9d8b6d..8bf7ba21 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: notation.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: notation.ml 13463 2010-09-24 22:21:29Z herbelin $ *) (*i*) open Util @@ -113,7 +113,7 @@ let subst_scope (subst,sc) = sc open Libobject -let discharge_scope (local,_,_ as o) = +let discharge_scope (_,(local,_,_ as o)) = if local then None else Some o let classify_scope (local,_,_ as o) = @@ -124,6 +124,7 @@ let (inScope,outScope) = cache_function = cache_scope; open_function = open_scope; subst_function = subst_scope; + discharge_function = discharge_scope; classify_function = classify_scope } let open_close_scope (local,opening,sc) = |