diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index d1eb50d370..59a58d643c 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1364,35 +1364,37 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert = 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,[]) + | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[]) + | PatVar Anonymous, NHole _ -> sigma,(false,0,[]) | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 -> let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in - sigma,(0,l) + sigma,(false,0,l) | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in - if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 + if le2 > List.length l1 then raise No_match else let l1',more_args = Util.List.chop le2 l1 in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) + (* Convention: notations to @f don't keep implicit arguments *) + let no_implicit = le2 = 0 in + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args) | r1, NList (x,y,iter,termin,revert) -> (match_cases_pattern_list (match_cases_pattern_no_more_args) - metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[]) + metas (terms,termlists,(),()) a1 x y iter termin revert),(false,0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = match match_cases_pattern metas sigma a1 a2 with - | out,(_,[]) -> out + | out,(_,_,[]) -> out | _ -> raise No_match let match_ind_pattern metas sigma ind pats a2 = match a2 with | NRef (GlobRef.IndRef r2) when eq_ind ind r2 -> - sigma,(0,pats) + sigma,(false,0,pats) | NApp (NRef (GlobRef.IndRef r2),l2) when eq_ind ind r2 -> let le2 = List.length l2 in @@ -1401,7 +1403,8 @@ let match_ind_pattern metas sigma ind pats a2 = raise No_match else let l1',more_args = Util.List.chop le2 pats in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) + let no_implicit = le2 = 0 in + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args) |_ -> raise No_match let reorder_canonically_substitution terms termlists metas = |