diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index fdf12faa04..2fa78bb9f3 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -781,7 +781,7 @@ let rec pat_binder_of_term t = DAst.map (function | GVar id -> PatVar (Name id) | GApp (t, l) -> begin match DAst.get t with - | GRef (ConstructRef cstr,_) -> + | GRef (GlobRef.ConstructRef cstr,_) -> let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) @@ -1337,10 +1337,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,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> + | 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) - | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) + | 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 @@ -1362,9 +1362,9 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 = let match_ind_pattern metas sigma ind pats a2 = match a2 with - | NRef (IndRef r2) when eq_ind ind r2 -> + | NRef (GlobRef.IndRef r2) when eq_ind ind r2 -> sigma,(0,pats) - | NApp (NRef (IndRef r2),l2) + | NApp (NRef (GlobRef.IndRef r2),l2) when eq_ind ind r2 -> let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats |