diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 3 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 32 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 14 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 4 |
5 files changed, 23 insertions, 32 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/dumpglob.ml b/interp/dumpglob.ml index 8d6a266c30..41d1da9694 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -20,31 +20,21 @@ let open_glob_file f = let close_glob_file () = close_out !glob_file -type glob_output_t = - | NoGlob - | StdOut - | MultFiles - | Feedback - | File of string +type glob_output = + | NoGlob + | Feedback + | MultFiles + | File of string let glob_output = ref NoGlob -let dump () = !glob_output != NoGlob +let dump () = !glob_output <> NoGlob -let noglob () = glob_output := NoGlob - -let dump_to_dotglob () = glob_output := MultFiles - -let dump_into_file f = - if String.equal f "stdout" then - (glob_output := StdOut; glob_file := stdout) - else - (glob_output := File f; open_glob_file f) - -let feedback_glob () = glob_output := Feedback +let set_glob_output mode = + glob_output := mode let dump_string s = - if dump () && !glob_output != Feedback then + if dump () && !glob_output != Feedback then output_string !glob_file s let start_dump_glob ~vfile ~vofile = @@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile = | File f -> open_glob_file f; output_string !glob_file "DIGEST NO\n" - | NoGlob | Feedback | StdOut -> + | NoGlob | Feedback -> () let end_dump_glob () = match !glob_output with | MultFiles | File _ -> close_glob_file () - | NoGlob | Feedback | StdOut -> () + | NoGlob | Feedback -> () let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 60d62a1cb2..2b6a116a01 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -8,19 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val open_glob_file : string -> unit -val close_glob_file : unit -> unit - val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool -val noglob : unit -> unit -val dump_into_file : string -> unit (** special handling of "stdout" *) +type glob_output = + | NoGlob + | Feedback + | MultFiles (* one glob file per .v file *) + | File of string (* Single file for all coqc arguments *) -val dump_to_dotglob : unit -> unit -val feedback_glob : unit -> unit +(* Default "NoGlob" *) +val set_glob_output : glob_output -> unit val pause : unit -> unit val continue : unit -> unit 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 |