diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coqProject_file.ml4 | 10 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 1 | ||||
| -rw-r--r-- | lib/envars.ml | 9 | ||||
| -rw-r--r-- | lib/envars.mli | 5 | ||||
| -rw-r--r-- | lib/flags.ml | 34 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | lib/pp.mli | 1 |
7 files changed, 25 insertions, 37 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 7a16605695..97aa90e07d 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -11,6 +11,7 @@ type project = { makefile : string option; install_kind : install option; use_ocamlopt : bool; + bypass_API : bool; v_files : string list; mli_files : string list; @@ -42,11 +43,12 @@ and install = | UserInstall (* TODO generate with PPX *) -let mk_project project_file makefile install_kind use_ocamlopt = { +let mk_project project_file makefile install_kind use_ocamlopt bypass_API = { project_file; makefile; install_kind; use_ocamlopt; + bypass_API; v_files = []; mli_files = []; @@ -166,6 +168,8 @@ let process_cmd_line orig_dir proj args = aux { proj with defs = proj.defs @ [v,def] } r | "-arg" :: a :: r -> aux { proj with extra_args = proj.extra_args @ [a] } r + | "-bypass-API" :: r -> + aux { proj with bypass_API = true } r | f :: r -> let f = CUnix.correct_path f orig_dir in let proj = @@ -185,11 +189,11 @@ let process_cmd_line orig_dir proj args = (******************************* API ************************************) let cmdline_args_to_project ~curdir args = - process_cmd_line curdir (mk_project None None None true) args + process_cmd_line curdir (mk_project None None None true false) args let read_project_file f = process_cmd_line (Filename.dirname f) - (mk_project (Some f) None (Some NoInstall) true) (parse f) + (mk_project (Some f) None (Some NoInstall) true false) (parse f) let rec find_project_file ~from ~projfile_name = let fname = Filename.concat from projfile_name in diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 8c8fc068a3..19fc9227ae 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -13,6 +13,7 @@ type project = { makefile : string option; install_kind : install option; use_ocamlopt : bool; + bypass_API : bool; v_files : string list; mli_files : string list; diff --git a/lib/envars.ml b/lib/envars.ml index 2f76183eb3..47baf66a69 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -202,14 +202,7 @@ let xdg_dirs ~warn = (* Print the configuration information *) -let coq_src_subdirs = [ - "config" ; "dev" ; "lib" ; "kernel" ; "library" ; - "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ; - "tactics" ; "toplevel" ; "printing" ; "intf" ; - "grammar" ; "ide" ; "stm"; "vernac" ; "API" ] @ - Coq_config.plugins_dirs - -let print_config ?(prefix_var_name="") f = +let print_config ?(prefix_var_name="") f coq_src_subdirs = let open Printf in fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0"); fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); diff --git a/lib/envars.mli b/lib/envars.mli index c8bbf17d96..edd13447fc 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -76,7 +76,4 @@ val xdg_data_dirs : (string -> unit) -> string list val xdg_dirs : warn : (string -> unit) -> string list (** {6 Prints the configuration information } *) -val print_config : ?prefix_var_name:string -> out_channel -> unit - -(** Directories in which coq sources are found *) -val coq_src_subdirs : string list +val print_config : ?prefix_var_name:string -> out_channel -> string list -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 6a3b7a4261..13539bced3 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -106,35 +106,27 @@ 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_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current +type compat_version = VOld | V8_5 | V8_6 | Current let compat_version = ref Current let version_compare v1 v2 = match v1, v2 with -| V8_2, V8_2 -> 0 -| V8_2, (V8_3 | V8_4 | V8_5 | V8_6 | Current) -> -1 -| V8_3, V8_2 -> 1 -| V8_3, V8_3 -> 0 -| V8_3, (V8_4 | V8_5 | V8_6 | Current) -> -1 -| V8_4, (V8_2 | V8_3) -> 1 -| V8_4, V8_4 -> 0 -| V8_4, (V8_5 | V8_6 | Current) -> -1 -| V8_5, (V8_2 | V8_3 | V8_4) -> 1 -| V8_5, V8_5 -> 0 -| V8_5, (V8_6 | Current) -> -1 -| V8_6, (V8_2 | V8_3 | V8_4 | V8_5) -> 1 -| V8_6, V8_6 -> 0 -| V8_6, Current -> -1 -| Current, Current -> 0 -| Current, (V8_2 | V8_3 | V8_4 | V8_5 | V8_6) -> 1 + | VOld, VOld -> 0 + | VOld, _ -> -1 + | _, VOld -> 1 + | V8_5, V8_5 -> 0 + | V8_5, _ -> -1 + | _, V8_5 -> 1 + | V8_6, V8_6 -> 0 + | V8_6, _ -> -1 + | _, V8_6 -> 1 + | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function - | V8_2 -> "8.2" - | V8_3 -> "8.3" - | V8_4 -> "8.4" + | VOld -> "old" | V8_5 -> "8.5" | V8_6 -> "8.6" | Current -> "current" @@ -157,7 +149,7 @@ let is_verbose () = not !quiet let auto_intros = ref true let make_auto_intros flag = auto_intros := flag -let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros +let is_auto_intros () = !auto_intros let universe_polymorphism = ref false let make_universe_polymorphism b = universe_polymorphism := b diff --git a/lib/flags.mli b/lib/flags.mli index e2cf09474e..0026aba2e3 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -77,7 +77,7 @@ val raw_print : bool ref (* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref -type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current +type compat_version = VOld | V8_5 | V8_6 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/lib/pp.mli b/lib/pp.mli index 7a191b01a8..45834dade5 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -13,6 +13,7 @@ (* `Pp.t` or `Pp.std_ppcmds` is the main pretty printing document type *) (* in the Coq system. Documents are composed laying out boxes, and *) (* users can add arbitrary tag metadata that backends are free *) +(* to interpret. *) (* *) (* The datatype has a public view to allow serialization or advanced *) (* uses, however regular users are _strongly_ warned againt its use, *) |