diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5151d2a1..c754f191 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1120,7 +1120,7 @@ let drop_notations_pattern looked_for = let (argscs,_) = find_remaining_scopes pats [] g in Some (g, List.map2 (in_pat_sc env) argscs pats, []) | NApp (NRef g,args) -> - ensure_kind top loc g; + test_kind top g; let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments loc; let pats1,pats2 = List.chop nvars pats in @@ -1142,7 +1142,11 @@ let drop_notations_pattern looked_for = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in begin match sorted_fields with | None -> RCPatAtom (loc, None) - | Some (_, head, pl) -> + | Some (n, head, pl) -> + let pl = + if !oldfashion_patterns then pl else + let pars = List.make n (CPatAtom (loc, None)) in + List.rev_append pars pl in match drop_syndef top env head pl with |Some (a,b,c) -> RCPatCstr(loc, a, b, c) |None -> raise (InternalizationError (loc,NotAConstructor head)) @@ -1214,7 +1218,8 @@ let drop_notations_pattern looked_for = List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl, List.map2 (in_pat_sc env) argscs2 args) | NList (x,_,iter,terminator,lassoc) -> - let () = assert (List.is_empty args) in + if not (List.is_empty args) then user_err_loc + (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = Id.Map.find x substlist in @@ -1893,7 +1898,7 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err_loc (loc,"internalize", explain_internalization_error e) -let interp_rawcontext_evars env evdref bl = +let interp_rawcontext_evars env evdref k bl = let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -1913,12 +1918,12 @@ let interp_rawcontext_evars env evdref bl = | Some b -> let c = understand_judgment_tcc env evdref b in let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env, d::params, succ n, impls)) - (env,[],1,[]) (List.rev bl) + (push_rel d env, d::params, n, impls)) + (env,[],k+1,[]) (List.rev bl) in (env, par), impls -let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) env evdref params = +let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_rawcontext_evars env evdref bl in + let x = interp_rawcontext_evars env evdref shift bl in int_env, x |