diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/control.ml | 2 | ||||
| -rw-r--r-- | lib/envars.ml | 4 | ||||
| -rw-r--r-- | lib/envars.mli | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 17 | ||||
| -rw-r--r-- | lib/flags.mli | 11 | ||||
| -rw-r--r-- | lib/loc.ml | 9 | ||||
| -rw-r--r-- | lib/loc.mli | 2 | ||||
| -rw-r--r-- | lib/pp.ml | 13 | ||||
| -rw-r--r-- | lib/stateid.ml | 2 | ||||
| -rw-r--r-- | lib/stateid.mli | 1 |
10 files changed, 21 insertions, 42 deletions
diff --git a/lib/control.ml b/lib/control.ml index e09068740d..ffb3584f1e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -57,7 +57,7 @@ let windows_timeout n f x e = done in let init = Unix.gettimeofday () in - let _id = Thread.create thread init in + let _id = CThread.create thread init in try let res = f x in let () = killed := true in diff --git a/lib/envars.ml b/lib/envars.ml index b5036e7340..8a75d9a552 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -110,11 +110,11 @@ let set_user_coqlib path = coqlib := Some path (** coqlib is now computed once during coqtop initialization *) -let set_coqlib ~fail = +let set_coqlib ~boot ~fail = match !coqlib with | Some _ -> () | None -> - let lib = if !Flags.boot then coqroot else guess_coqlib fail in + let lib = if boot then coqroot else guess_coqlib fail in coqlib := Some lib let coqlib () = Option.default "" !coqlib diff --git a/lib/envars.mli b/lib/envars.mli index ebf86d0650..21365c48f6 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -39,7 +39,7 @@ val datadir : unit -> string val configdir : unit -> string (** [set_coqlib] must be runned once before any access to [coqlib] *) -val set_coqlib : fail:(string -> string) -> unit +val set_coqlib : boot:bool -> fail:(string -> string) -> unit (** [set_user_coqlib path] sets the coqlib directory explicitedly. *) val set_user_coqlib : string -> unit diff --git a/lib/flags.ml b/lib/flags.ml index ae4d337ded..768d359cce 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -41,8 +41,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let boot = ref false - let record_aux_file = ref false let test_mode = ref false @@ -66,7 +64,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_7 | V8_8 | Current +type compat_version = V8_7 | V8_8 | V8_9 | Current let compat_version = ref Current @@ -77,6 +75,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_8, V8_8 -> 0 | V8_8, _ -> -1 | _, V8_8 -> 1 + | V8_9, V8_9 -> 0 + | V8_9, _ -> -1 + | _, V8_9 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -85,6 +86,7 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | V8_7 -> "8.7" | V8_8 -> "8.8" + | V8_9 -> "8.9" | Current -> "current" (* Translate *) @@ -103,12 +105,6 @@ let polymorphic_inductive_cumulativity = ref false let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity -(** [program_mode] tells that Program mode has been activated, either - globally via [Set Program] or locally via the Program command prefix. *) - -let program_mode = ref false -let is_program_mode () = !program_mode - let warn = ref true let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x @@ -120,8 +116,5 @@ let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level -(* Native code compilation for conversion and normalization *) -let output_native_objects = ref false - let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli index d883cf1e30..4ef5fb4445 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -31,8 +31,6 @@ (** Command-line flags *) -val boot : bool ref - (** Set by coqtop to tell the kernel to output to the aux file; will be eventually removed by cleanups such as PR#1103 *) val record_aux_file : bool ref @@ -58,7 +56,7 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_7 | V8_8 | Current +type compat_version = V8_7 | V8_8 | V8_9 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool @@ -77,10 +75,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit -(* Miscellaneus flags for vernac *) -val program_mode : bool ref -val is_program_mode : unit -> bool - (** Global polymorphic inductive cumulativity flag. *) val make_polymorphic_inductive_cumulativity : bool -> unit val is_polymorphic_inductive_cumulativity : unit -> bool @@ -116,9 +110,6 @@ val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(** When producing vo objects, also compile the native-code version *) -val output_native_objects : bool ref - (** Global profile_ltac flag *) val profile_ltac : bool ref val profile_ltac_cutoff : float ref diff --git a/lib/loc.ml b/lib/loc.ml index c08648911b..66b7a7da70 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -22,19 +22,17 @@ type t = { bol_pos_last : int; (** position of the beginning of end line *) bp : int; (** start position *) ep : int; (** end position *) - comm : string; (** start comment *) - ecomm : string (** end comment *) } let create fname line_nb bol_pos bp ep = { fname = fname; line_nb = line_nb; bol_pos = bol_pos; line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; - comm = ""; ecomm = "" } +} let make_loc (bp, ep) = { fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = bp; ep = ep; - comm = ""; ecomm = "" } +} let mergeable loc1 loc2 = loc1.fname = loc2.fname @@ -50,7 +48,7 @@ let merge loc1 loc2 = line_nb_last = loc2.line_nb_last; bol_pos_last = loc2.bol_pos_last; bp = loc1.bp; ep = loc2.ep; - comm = loc1.comm; ecomm = loc2.comm } + } else loc1 else if loc2.ep < loc1.ep then { fname = loc2.fname; @@ -59,7 +57,6 @@ let merge loc1 loc2 = line_nb_last = loc1.line_nb_last; bol_pos_last = loc1.bol_pos_last; bp = loc2.bp; ep = loc1.ep; - comm = loc2.comm; ecomm = loc1.comm } else loc2 diff --git a/lib/loc.mli b/lib/loc.mli index c46311b639..23df1ebd9a 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -22,8 +22,6 @@ type t = { bol_pos_last : int; (** position of the beginning of end line *) bp : int; (** start position *) ep : int; (** end position *) - comm : string; (** start comment *) - ecomm : string (** end comment *) } (** {5 Location manipulation} *) @@ -284,15 +284,12 @@ let pr_vertical_list pr = function [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *) let prvecti_with_sep sep elem v = - let rec pr i = - if Int.equal i 0 then - elem 0 v.(0) - else - let r = pr (i-1) and s = sep () and e = elem i v.(i) in - r ++ s ++ e + let v = CArray.mapi (fun i x -> + let pp = if i = 0 then mt() else sep() in + pp ++ elem i x) + v in - let n = Array.length v in - if Int.equal n 0 then mt () else pr (n - 1) + seq (Array.to_list v) (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) diff --git a/lib/stateid.ml b/lib/stateid.ml index 5485c4bf19..8f45f3605d 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -27,6 +27,8 @@ let get exn = Exninfo.get exn state_id_info let equal = Int.equal let compare = Int.compare +let print id = Pp.int id + module Self = struct type t = int let compare = compare diff --git a/lib/stateid.mli b/lib/stateid.mli index 5d4b71a354..f6ce7ddc40 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -20,6 +20,7 @@ val initial : t val dummy : t val fresh : unit -> t val to_string : t -> string +val print : t -> Pp.t val of_int : int -> t val to_int : t -> int |