diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 3 | ||||
| -rw-r--r-- | interp/impargs.mli | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 6 |
3 files changed, 6 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb5fd5294f..7792eff664 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -478,7 +478,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function if is_inactive_rule keyrule then raise No_match; let loc = t.loc in match DAst.get t with - | PatCstr (cstr,_,na) -> + | PatCstr (cstr,args,na) -> + let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in let p = apply_notation_to_pattern ?loc (ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na diff --git a/interp/impargs.mli b/interp/impargs.mli index 1eeb8e41ae..103a4f9e95 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -130,7 +130,7 @@ val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list -val projection_implicits : env -> projection -> implicit_status list -> +val projection_implicits : env -> Projection.t -> implicit_status list -> implicit_status list val select_impargs_size : int -> implicits_list list -> implicit_status list diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index a0d69ce796..a76f820941 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -210,7 +210,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',na = protect g e na in GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> - let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) -> + let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) -> let e,na = protect g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in @@ -1335,10 +1335,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = match DAst.get a1, a2 with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) - | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> + | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in sigma,(0,l) - | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) + | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in |