diff options
| author | Maxime Dénès | 2019-04-05 10:09:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:44 +0200 |
| commit | 84fa6a47a7ca5fbb5c83595ea2491f821b0c9d86 (patch) | |
| tree | 1868fc448cfd325effd6a76514c9d4fab052435c /interp/notation_ops.ml | |
| parent | 61d53a17c594de1ea37b37f6215319d996ec31ea (diff) | |
Remove calls to Global.env in Glob_ops
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7d7e10a05b..1f1cf4506f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1292,7 +1292,7 @@ let match_notation_constr u c (metas,pat) = | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with | [pat] -> - let v = glob_constr_of_cases_pattern pat in + let v = glob_constr_of_cases_pattern (Global.env()) pat in ((v,scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) -> @@ -1333,11 +1333,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = | 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 -> - let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + 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) 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 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 then |