diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 3 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 4 |
3 files changed, 5 insertions, 4 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3f216b0d63..b4798127f9 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -625,7 +625,8 @@ let interp_univ_constraints env evd cstrs = let interp_univ_decl env decl = let open UState in let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in + let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env) + (Environ.universes env) pl) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; univdecl_extensible_instance = decl.univdecl_extensible_instance; diff --git a/interp/notation.ml b/interp/notation.ml index a78bc60e83..ea2173860d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1205,7 +1205,7 @@ let interp_notation ?loc ntn local_scopes = let scopes = make_current_scopes local_scopes in try let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in - Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation; + Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation; n.not_interp, (n.not_location, sc) with Not_found -> user_err ?loc diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 302bb6ece2..9dded8656c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -100,7 +100,7 @@ let warn_deprecated_syntactic_definition = let search_syntactic_definition ?loc kn = let syndef = KNmap.find kn !syntax_table in let def = out_pat syndef.syndef_pattern in - Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation; + Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; def let search_filtered_syntactic_definition ?loc filter kn = @@ -108,5 +108,5 @@ let search_filtered_syntactic_definition ?loc filter kn = let def = out_pat syndef.syndef_pattern in let res = filter def in if Option.has_some res then - Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation; + Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; res |