aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/declareDef.ml4
-rw-r--r--vernac/declaremods.ml4
-rw-r--r--vernac/g_vernac.mlg66
-rw-r--r--vernac/indschemes.ml6
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/library.ml4
-rw-r--r--vernac/loadpath.ml56
-rw-r--r--vernac/loadpath.mli29
-rw-r--r--vernac/metasyntax.ml22
-rw-r--r--vernac/metasyntax.mli6
-rw-r--r--vernac/mltop.ml5
-rw-r--r--vernac/mltop.mli2
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/ppvernac.ml36
-rw-r--r--vernac/topfmt.ml4
-rw-r--r--vernac/vernacentries.ml23
-rw-r--r--vernac/vernacexpr.ml16
-rw-r--r--vernac/vernacextend.ml10
-rw-r--r--vernac/vernacinterp.ml6
-rw-r--r--vernac/vernacstate.ml2
21 files changed, 152 insertions, 159 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b92c9e9b71..16b9e07fb2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -60,7 +60,9 @@ let add_instance check inst =
let local = is_local_for_hint inst in
add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local
inst.is_info poly;
- List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path
+ List.iter (fun (path, pri, c) ->
+ let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in
+ add_instance_hint h path
local pri poly)
(build_subclasses ~check:(check && not (isVarRef inst.is_impl))
(Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index e57c324c9a..2b6f987fa6 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -37,9 +37,9 @@ module Hook = struct
let call ?hook ?fix_exn x =
try Option.iter (fun hook -> CEphemeron.get hook x) hook
with e when CErrors.noncritical e ->
- let e = CErrors.push e in
+ let e = Exninfo.capture e in
let e = Option.cata (fun fix -> fix e) e fix_exn in
- Util.iraise e
+ Exninfo.iraise e
end
(* Locality stuff *)
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index c816a4eb4f..e645fc552b 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -935,9 +935,9 @@ let protect_summaries f =
try f fs
with reraise ->
(* Something wrong: undo the whole process *)
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
let () = Summary.unfreeze_summaries fs in
- iraise reraise
+ Exninfo.iraise reraise
let start_module export id args res =
protect_summaries (RawModOps.start_module export id args res)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index def4ed942a..c1414c552a 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -22,7 +22,6 @@ open Extend
open Decls
open Declaremods
open Namegen
-open Tok (* necessary for camlp5 *)
open Pcoq
open Pcoq.Prim
@@ -45,11 +44,12 @@ let quoted_attributes = Entry.create "vernac:quoted_attributes"
let class_rawexpr = Entry.create "vernac:class_rawexpr"
let thm_token = Entry.create "vernac:thm_token"
let def_body = Entry.create "vernac:def_body"
-let decl_notation = Entry.create "vernac:decl_notation"
+let decl_notations = Entry.create "vernac:decl_notations"
let record_field = Entry.create "vernac:record_field"
let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
let section_subset_expr = Entry.create "vernac:section_subset_expr"
let scope_delimiter = Entry.create "vernac:scope_delimiter"
+let only_parsing = Entry.create "vernac:only_parsing"
let make_bullet s =
let open Proof_bullet in
@@ -177,7 +177,7 @@ let name_of_ident_decl : ident_decl -> name_decl =
(* Gallina declarations *)
GRAMMAR EXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
- record_field decl_notation rec_definition ident_decl univ_decl;
+ record_field decl_notations rec_definition ident_decl univ_decl;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
@@ -377,15 +377,17 @@ GRAMMAR EXTEND Gram
[ [ IDENT "Eval"; r = red_expr; "in" -> { Some r }
| -> { None } ] ]
;
- one_decl_notation:
- [ [ ntn = ne_lstring; ":="; c = constr;
- scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> { (ntn,c,scopt) } ] ]
+ decl_notation:
+ [ [ ntn = ne_lstring; ":="; c = constr; b = only_parsing;
+ scopt = OPT [ ":"; sc = IDENT -> { sc } ] ->
+ { { decl_ntn_string = ntn; decl_ntn_interp = c;
+ decl_ntn_only_parsing = b; decl_ntn_scope = scopt } } ] ]
;
decl_sep:
[ [ IDENT "and" -> { () } ] ]
;
- decl_notation:
- [ [ "where"; l = LIST1 one_decl_notation SEP decl_sep -> { l }
+ decl_notations:
+ [ [ "where"; l = LIST1 decl_notation SEP decl_sep -> { l }
| -> { [] } ] ]
;
(* Inductives and records *)
@@ -397,7 +399,7 @@ GRAMMAR EXTEND Gram
[ [ oc = opt_coercion; id = ident_decl; indpar = binders;
extrapar = OPT [ "|"; p = binders -> { p } ];
c = OPT [ ":"; c = lconstr -> { c } ];
- lc=opt_constructors_or_fields; ntn = decl_notation ->
+ lc=opt_constructors_or_fields; ntn = decl_notations ->
{ (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
;
constructor_list_or_record_decl:
@@ -424,14 +426,14 @@ GRAMMAR EXTEND Gram
[ [ id_decl = ident_decl;
bl = binders_fixannot;
rtype = type_cstr;
- body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation ->
+ body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notations ->
{ let binders, rec_order = bl in
{fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
} ] ]
;
corec_definition:
[ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
- body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation ->
+ body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations ->
{ {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
} ]]
;
@@ -467,7 +469,7 @@ GRAMMAR EXTEND Gram
record_field:
[ [ attr = LIST0 quoted_attributes ;
bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
- rf_notation = decl_notation -> {
+ rf_notation = decl_notations -> {
let rf_canonical = attr |> List.flatten |> parse canonical_field in
let rf_subclass, rf_decl = bd in
rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
@@ -531,16 +533,12 @@ END
{
-let only_starredidentrefs =
- Pcoq.Entry.of_parser "test_only_starredidentrefs"
- (fun _ strm ->
- let rec aux n =
- match Util.stream_nth n strm with
- | KEYWORD "." -> ()
- | KEYWORD ")" -> ()
- | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
- | _ -> raise Stream.Failure in
- aux 0)
+let test_only_starredidentrefs =
+ let open Pcoq.Lookahead in
+ to_entry "test_only_starredidentrefs" begin
+ lk_list (lk_ident <+> lk_kws ["Type"; "*"]) >> (lk_kws [".";")"])
+ end
+
let starredidentreflist_to_expr l =
match l with
| [] -> SsEmpty
@@ -670,7 +668,7 @@ GRAMMAR EXTEND Gram
;
(* Proof using *)
section_subset_expr:
- [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+ [ [ test_only_starredidentrefs; l = LIST0 starredidentref ->
{ starredidentreflist_to_expr l }
| e = ssexpr -> { e } ]]
;
@@ -688,9 +686,9 @@ GRAMMAR EXTEND Gram
| e1 = ssexpr; "+"; e2 = ssexpr-> { SsUnion(e1,e2) } ]
| "0"
[ i = starredidentref -> { i }
- | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+ | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"->
{ starredidentreflist_to_expr l }
- | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+ | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
{ SsFwdClose(starredidentreflist_to_expr l) }
| "("; e = ssexpr; ")"-> { e }
| "("; e = ssexpr; ")"; "*" -> { SsFwdClose e } ] ]
@@ -917,10 +915,11 @@ GRAMMAR EXTEND Gram
| IDENT "Locate"; l = locatable -> { VernacLocate l }
(* Managing load paths *)
- | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath ->
- { VernacAddLoadPath (false, dir, alias) }
- | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string;
- alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) }
+ | IDENT "Add"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath ->
+ { VernacAddLoadPath { implicit = false; logical_path; physical_path } }
+ | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath ->
+ { VernacAddLoadPath { implicit = true; logical_path; physical_path } }
+
| IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
{ VernacRemoveLoadPath dir }
@@ -939,9 +938,7 @@ GRAMMAR EXTEND Gram
| IDENT "Inspect"; n = natural -> { VernacPrint (PrintInspect n) }
| IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
- { VernacAddMLPath (false, dir) }
- | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
- { VernacAddMLPath (true, dir) }
+ { VernacAddMLPath dir }
(* For acting on parameter tables *)
| "Set"; table = option_table; v = option_setting ->
@@ -1075,9 +1072,6 @@ GRAMMAR EXTEND Gram
option_table:
[ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
;
- as_dirpath:
- [ [ d = OPT [ "as"; d = dirpath -> { d } ] -> { d } ] ]
- ;
ne_in_or_out_modules:
[ [ IDENT "inside"; l = LIST1 global -> { SearchInside l }
| IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ]
@@ -1154,7 +1148,7 @@ GRAMMAR EXTEND Gram
(* Grammar extensions *)
GRAMMAR EXTEND Gram
- GLOBAL: syntax;
+ GLOBAL: syntax only_parsing;
syntax:
[ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 227d2f1554..80616ecc2a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -118,7 +118,7 @@ let alarm what internal msg =
let try_declare_scheme what f internal names kn =
try f internal names kn
with e ->
- let e = CErrors.push e in
+ let e = Exninfo.capture e in
let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in
let msg = match extract_exn (fst e) with
| ParameterWithoutEquality cst ->
@@ -166,11 +166,11 @@ let try_declare_scheme what f internal names kn =
| e when CErrors.noncritical e ->
alarm what internal
(str "Unexpected error during scheme creation: " ++ CErrors.print e)
- | _ -> iraise e
+ | _ -> Exninfo.iraise e
in
match msg with
| None -> ()
- | Some msg -> iraise (UserError (None, msg), snd e)
+ | Some msg -> Exninfo.iraise (UserError (None, msg), snd e)
let beq_scheme_msg mind =
let mib = Global.lookup_mind mind in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index f7606f4ede..68f4f55d0e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -375,8 +375,8 @@ let finish_proved env sigma idopt po info =
(* This takes care of the implicits and hook for the current constant*)
process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms
with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- iraise (fix_exn e)
+ let e = Exninfo.capture e in
+ Exninfo.iraise (fix_exn e)
in ()
| _ ->
CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term")
diff --git a/vernac/library.ml b/vernac/library.ml
index 0f7e7d2aa0..5aff86c50c 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -440,11 +440,11 @@ let save_library_base f sum lib univs tasks proofs =
System.marshal_out_segment f ch (proofs : seg_proofs);
close_out ch
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
close_out ch;
Feedback.msg_warning (str "Removed file " ++ str f);
Sys.remove f;
- iraise reraise
+ Exninfo.iraise reraise
type ('document,'counters) todo_proofs =
| ProofsTodoNone (* for .vo *)
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index 506b3bc505..38aa42c349 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -218,24 +218,18 @@ let try_locate_absolute_library dir =
(** { 5 Extending the load path } *)
-(* Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
- unix_path : string; (* Filesystem path containing vo/ml files *)
- coq_path : DP.t; (* Coq prefix for the path *)
- implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *)
- has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *)
-}
-
-type coq_path_spec =
- | VoPath of vo_path_spec
- | MlPath of string
-
-type coq_path = {
- path_spec: coq_path_spec;
- recursive: bool;
-}
+type vo_path =
+ { unix_path : string
+ (** Filesystem path containing vo/ml files *)
+ ; coq_path : DP.t
+ (** Coq prefix for the path *)
+ ; implicit : bool
+ (** [implicit = true] avoids having to qualify with [coq_path] *)
+ ; has_ml : bool
+ (** If [has_ml] is true, the directory will also be added to the ml include path *)
+ ; recursive : bool
+ (** [recursive] will determine whether we explore sub-directories *)
+ }
let warn_cannot_open_path =
CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
@@ -255,9 +249,10 @@ let convert_string d =
warn_cannot_use_directory d;
raise Exit
-let add_vo_path ~recursive lp =
+let add_vo_path lp =
let unix_path = lp.unix_path in
let implicit = lp.implicit in
+ let recursive = lp.recursive in
if System.exists_dir unix_path then
let dirs = if recursive then System.all_subdirs ~unix_path else [] in
let prefix = DP.repr lp.coq_path in
@@ -268,22 +263,17 @@ let add_vo_path ~recursive lp =
with Exit -> None
in
let dirs = List.map_filter convert_dirs dirs in
- let add_ml_dir = Mltop.add_ml_dir ~recursive:false in
- let () = match lp.has_ml with
- | AddNoML -> ()
- | AddTopML ->
- Mltop.add_ml_dir ~recursive:false unix_path
- | AddRecML ->
- List.iter (fun (lp,_) -> add_ml_dir lp) dirs;
- add_ml_dir unix_path in
+ let () =
+ if lp.has_ml && not lp.recursive then
+ Mltop.add_ml_dir unix_path
+ else if lp.has_ml && lp.recursive then
+ (List.iter (fun (lp,_) -> Mltop.add_ml_dir lp) dirs;
+ Mltop.add_ml_dir unix_path)
+ else
+ ()
+ in
let add (path, dir) = add_load_path path ~implicit dir in
let () = List.iter add dirs in
add_load_path unix_path ~implicit lp.coq_path
else
warn_cannot_open_path unix_path
-
-let add_coq_path { recursive; path_spec } = match path_spec with
- | VoPath lp ->
- add_vo_path ~recursive lp
- | MlPath dir ->
- Mltop.add_ml_dir ~recursive dir
diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli
index 47d2d34125..68212b9a47 100644
--- a/vernac/loadpath.mli
+++ b/vernac/loadpath.mli
@@ -64,26 +64,17 @@ val try_locate_absolute_library : DirPath.t -> string
(** {6 Extending the Load Path } *)
(** Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
- unix_path : string;
+type vo_path =
+ { unix_path : string
(** Filesystem path containing vo/ml files *)
- coq_path : Names.DirPath.t;
+ ; coq_path : DirPath.t
(** Coq prefix for the path *)
- implicit : bool;
+ ; implicit : bool
(** [implicit = true] avoids having to qualify with [coq_path] *)
- has_ml : add_ml;
- (** If [has_ml] is true, the directory will also be search for plugins *)
-}
-
-type coq_path_spec =
- | VoPath of vo_path_spec
- | MlPath of string
-
-type coq_path = {
- path_spec: coq_path_spec;
- recursive: bool;
-}
+ ; has_ml : bool
+ (** If [has_ml] is true, the directory will also be added to the ml include path *)
+ ; recursive : bool
+ (** [recursive] will determine whether we explore sub-directories *)
+ }
-val add_coq_path : coq_path -> unit
+val add_vo_path : vo_path -> unit
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3937f887ad..33fd14a731 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1466,9 +1466,9 @@ let with_lib_stk_protection f x =
let fs = Lib.freeze () in
try let a = f x in Lib.unfreeze fs; a
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
let () = Lib.unfreeze fs in
- iraise reraise
+ Exninfo.iraise reraise
let with_syntax_protection f x =
with_lib_stk_protection
@@ -1654,13 +1654,23 @@ let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
(* Notations with only interpretation *)
-let add_notation_interpretation env ({CAst.loc;v=df},c,sc) =
- let df' = add_notation_interpretation_core ~local:false df env c sc false false None in
+let add_notation_interpretation env decl_ntn =
+ let
+ { decl_ntn_string = { CAst.loc ; v = df };
+ decl_ntn_interp = c;
+ decl_ntn_only_parsing = onlyparse;
+ decl_ntn_scope = sc } = decl_ntn in
+ let df' = add_notation_interpretation_core ~local:false df env c sc onlyparse false None in
Dumpglob.dump_notation (loc,df') sc true
-let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) =
+let set_notation_for_interpretation env impls decl_ntn =
+ let
+ { decl_ntn_string = { CAst.v = df };
+ decl_ntn_interp = c;
+ decl_ntn_only_parsing = onlyparse;
+ decl_ntn_scope = sc } = decl_ntn in
(try ignore
- (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ());
+ (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc onlyparse false None) ());
with NoSyntaxRule ->
user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index e3e733a4b7..d76820b033 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -37,12 +37,12 @@ val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit
(** Add only the interpretation of a notation that already has pa/pp rules *)
val add_notation_interpretation :
- env -> (lstring * constr_expr * scope_name option) -> unit
+ env -> decl_notation -> unit
(** Add a notation interpretation for supporting the "where" clause *)
-val set_notation_for_interpretation : env -> Constrintern.internalization_env ->
- (lstring * constr_expr * scope_name option) -> unit
+val set_notation_for_interpretation :
+ env -> Constrintern.internalization_env -> decl_notation -> unit
(** Add only the parsing/printing rule of a notation *)
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 5046248e11..671dae7876 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -128,11 +128,6 @@ let add_ml_dir s =
| WithoutTop when has_dynlink -> keep_copy_mlpath s
| _ -> ()
-(* For Rec Add ML Path (-R) *)
-let add_ml_dir ~recursive unix_path =
- let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in
- List.iter (fun (lp,_) -> add_ml_dir lp) dirs
-
(* convertit un nom quelconque en nom de fichier ou de module *)
let mod_of_name name =
if Filename.check_suffix name ".cmo" then
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 271772d7ba..633a5c241d 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -32,7 +32,7 @@ val ocaml_toploop : unit -> unit
(** {5 ML Dynlink} *)
(** Adds a dir to the plugin search path *)
-val add_ml_dir : recursive:bool -> string -> unit
+val add_ml_dir : string -> unit
(** Tests if we can load ML files *)
val has_dynlink : bool
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 76dbf1ad5a..27eb821a6a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -428,7 +428,7 @@ let solve_by_tac ?loc name evi t poly ctx =
Some (body, entry.Declare.proof_entry_type, ctx')
with
| Refiner.FailError (_, s) as exn ->
- let _ = CErrors.push exn in
+ let _ = Exninfo.capture exn in
user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
(* If the proof is open we absorb the error and leave the obligation open *)
| Proof.OpenProof _ ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 314c423f65..84ae04e4cc 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -297,11 +297,6 @@ open Pputils
| { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt()
| _ as c -> brk(0,2) ++ str" :" ++ pr_c c
- let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
- fnl () ++ keyword "where " ++ qs ntn ++ str " := "
- ++ Flags.without_option Flags.beautify prc c ++
- pr_opt (fun sc -> str ": " ++ str sc) scopt
-
let pr_binders_arg =
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -418,6 +413,21 @@ let string_of_theorem_kind = let open Decls in function
| l -> spc() ++
hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+ let pr_only_parsing_clause onlyparsing =
+ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])
+
+ let pr_decl_notation prc decl_ntn =
+ let open Vernacexpr in
+ let
+ { decl_ntn_string = {CAst.loc;v=ntn};
+ decl_ntn_interp = c;
+ decl_ntn_only_parsing = onlyparsing;
+ decl_ntn_scope = scopt } = decl_ntn in
+ fnl () ++ keyword "where " ++ qs ntn ++ str " := "
+ ++ Flags.without_option Flags.beautify prc c
+ ++ pr_only_parsing_clause onlyparsing
+ ++ pr_opt (fun sc -> str ": " ++ str sc) scopt
+
let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } =
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -1016,22 +1026,18 @@ let string_of_definition_object_kind = let open Decls in function
return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
(* Auxiliary file and library management *)
- | VernacAddLoadPath (fl,s,d) ->
+ | VernacAddLoadPath { implicit; physical_path; logical_path } ->
return (
hov 2
(keyword "Add" ++
- (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
- keyword "LoadPath" ++ spc() ++ qs s ++
- (match d with
- | None -> mt()
- | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
- )
+ (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++
+ keyword "LoadPath" ++ spc() ++ qs physical_path ++
+ spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path))
| VernacRemoveLoadPath s ->
return (keyword "Remove LoadPath" ++ qs s)
- | VernacAddMLPath (fl,s) ->
+ | VernacAddMLPath (s) ->
return (
keyword "Add"
- ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
++ keyword "ML Path"
++ qs s
)
@@ -1061,7 +1067,7 @@ let string_of_definition_object_kind = let open Decls in function
hov 2
(keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
- pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
+ pr_only_parsing_clause onlyparsing)
)
| VernacArguments (q, args, more_implicits, mods) ->
return (
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index de02f7ecfb..509c164af8 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -361,7 +361,7 @@ let in_phase ~phase f x =
with exn ->
let iexn = Exninfo.capture exn in
default_phase := op;
- Util.iraise iexn
+ Exninfo.iraise iexn
let pr_loc loc =
let fname = loc.Loc.fname in
@@ -394,7 +394,7 @@ let pr_phase ?loc () =
None
let print_err_exn any =
- let (e, info) = CErrors.push any in
+ let (e, info) = Exninfo.capture any in
let loc = Loc.get_loc info in
let pre_hdr = pr_phase ?loc () in
let msg = CErrors.iprint (e, info) ++ fnl () in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2eb1aa39b0..953faf6fdb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -342,9 +342,9 @@ let dump_universes_gen prl g s =
close ();
str "Universes written to file \"" ++ str s ++ str "\"."
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
close ();
- iraise reraise
+ Exninfo.iraise reraise
let universe_subgraph ?loc g univ =
let open Univ in
@@ -1120,20 +1120,17 @@ let vernac_set_used_variables ~pstate e : Proof_global.t =
let expand filename =
Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
-let vernac_add_loadpath implicit pdir ldiropt =
+let vernac_add_loadpath ~implicit pdir coq_path =
let open Loadpath in
let pdir = expand pdir in
- let alias = Option.default Libnames.default_root_prefix ldiropt in
- add_coq_path { recursive = true;
- path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } }
+ add_vo_path { unix_path = pdir; coq_path; has_ml = true; implicit; recursive = true }
let vernac_remove_loadpath path =
Loadpath.remove_load_path (expand path)
(* Coq syntax for ML or system commands *)
-let vernac_add_ml_path isrec path =
- let open Loadpath in
- add_coq_path { recursive = isrec; path_spec = MlPath (expand path) }
+let vernac_add_ml_path path =
+ Mltop.add_ml_dir (expand path)
let vernac_declare_ml_module ~local l =
let local = Option.default false local in
@@ -2106,18 +2103,18 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
unsupported_attributes atts;
vernac_solve_existential ~pstate n c)
(* Auxiliary file and library management *)
- | VernacAddLoadPath (isrec,s,alias) ->
+ | VernacAddLoadPath { implicit; physical_path; logical_path } ->
VtDefault(fun () ->
unsupported_attributes atts;
- vernac_add_loadpath isrec s alias)
+ vernac_add_loadpath ~implicit physical_path logical_path)
| VernacRemoveLoadPath s ->
VtDefault(fun () ->
unsupported_attributes atts;
vernac_remove_loadpath s)
- | VernacAddMLPath (isrec,s) ->
+ | VernacAddMLPath (s) ->
VtDefault(fun () ->
unsupported_attributes atts;
- vernac_add_ml_path isrec s)
+ vernac_add_ml_path s)
| VernacDeclareMLModule l ->
VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l)
| VernacChdir s ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 45018a246c..7169ea834a 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -98,7 +98,6 @@ type search_restriction =
| SearchInside of qualid list
| SearchOutside of qualid list
-type rec_flag = bool (* true = Rec; false = NoRec *)
type verbose_flag = bool (* true = Verbose; false = Silent *)
type coercion_flag = bool (* true = AddCoercion false = NoCoercion *)
type instance_flag = bool option
@@ -129,7 +128,12 @@ type definition_expr =
| DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
* constr_expr option
-type decl_notation = lstring * constr_expr * scope_name option
+type decl_notation =
+ { decl_ntn_string : lstring
+ ; decl_ntn_interp : constr_expr
+ ; decl_ntn_only_parsing : bool
+ ; decl_ntn_scope : scope_name option
+ }
type 'a fix_expr_gen =
{ fname : lident
@@ -363,9 +367,13 @@ type nonrec vernac_expr =
| VernacSolveExistential of int * constr_expr
(* Auxiliary file and library management *)
- | VernacAddLoadPath of rec_flag * string * DirPath.t option
+ | VernacAddLoadPath of { implicit : bool
+ ; physical_path : CUnix.physical_path
+ ; logical_path : DirPath.t
+ }
+
| VernacRemoveLoadPath of string
- | VernacAddMLPath of rec_flag * string
+ | VernacAddMLPath of string
| VernacDeclareMLModule of string list
| VernacChdir of string option
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index f41df06f85..e0afb7f483 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -109,11 +109,11 @@ let type_vernac opn converted_args ~atts =
phase := "Executing command";
hunk ~atts
with
- | reraise ->
- let reraise = CErrors.push reraise in
- if !Flags.debug then
- Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase);
- iraise reraise
+ | reraise ->
+ let reraise = Exninfo.capture reraise in
+ if !Flags.debug then
+ Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase);
+ Exninfo.iraise reraise
(** VERNAC EXTEND registering *)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1ec09b6beb..8083098022 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -96,7 +96,7 @@ let with_fail f : (Pp.t, unit) result =
(* Fail Timeout is a common pattern so we need to support it. *)
| e when CErrors.noncritical e || e = CErrors.Timeout ->
(* The error has to be printed in the failing state *)
- Ok CErrors.(iprint (push e))
+ Ok CErrors.(iprint (Exninfo.capture e))
(* We restore the state always *)
let with_fail ~st f =
@@ -262,10 +262,10 @@ let interp_gen ~verbosely ~st ~interp_fn cmd =
Vernacstate.freeze_interp_state ~marshallable:false
) st
with exn ->
- let exn = CErrors.push exn in
+ let exn = Exninfo.capture exn in
let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
Vernacstate.invalidate_cache ();
- Util.iraise exn
+ Exninfo.iraise exn
(* Regular interp *)
let interp ?(verbosely=true) ~st cmd =
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 3c70961e06..59557a60a6 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -21,7 +21,7 @@ module Parser = struct
Flags.with_option Flags.we_are_parsing (fun () ->
try Pcoq.Entry.parse entry pa
with e when CErrors.noncritical e ->
- let (e, info) = CErrors.push e in
+ let (e, info) = Exninfo.capture e in
Exninfo.iraise (e, info))
()
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:21:45 +0000