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/constrintern.ml | |
| parent | 61d53a17c594de1ea37b37f6215319d996ec31ea (diff) | |
Remove calls to Global.env in Glob_ops
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 59feb46dc1..d4555707c4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -753,7 +753,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with - | [pat] -> (glob_constr_of_cases_pattern pat, None) + | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in let terms = Id.Map.fold mk_env terms Id.Map.empty in @@ -815,7 +815,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with - | [pat] -> glob_constr_of_cases_pattern pat + | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try |