aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CREDITS2
-rw-r--r--Makefile.common4
-rw-r--r--_tags1
-rw-r--r--dev/ocamldebug-coq.template2
-rw-r--r--dev/printers.mllib2
-rw-r--r--intf/vernacexpr.mli (renamed from toplevel/vernacexpr.ml)158
-rw-r--r--lib/errors.ml2
-rw-r--r--lib/errors.mli2
-rw-r--r--parsing/g_ltac.ml41
-rw-r--r--parsing/g_obligations.ml42
-rw-r--r--parsing/g_proofs.ml41
-rw-r--r--parsing/g_vernac.ml41
-rw-r--r--parsing/grammar.mllib2
-rw-r--r--plugins/firstorder/g_ground.ml42
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/rewrite.ml414
-rw-r--r--toplevel/ide_slave.ml6
-rw-r--r--toplevel/locality.ml112
-rw-r--r--toplevel/locality.mli61
-rw-r--r--toplevel/toplevel.ml13
-rw-r--r--toplevel/toplevel.mllib2
-rw-r--r--toplevel/vernac.ml15
-rw-r--r--toplevel/vernac.mli3
-rw-r--r--toplevel/vernacentries.ml2
-rw-r--r--toplevel/vernacinterp.ml1
25 files changed, 235 insertions, 178 deletions
diff --git a/CREDITS b/CREDITS
index 35057ea8f..c654db2ee 100644
--- a/CREDITS
+++ b/CREDITS
@@ -12,7 +12,7 @@ The "Coq proof assistant" was jointly developed by
All files of the "Coq proof assistant" in directories or sub-directories of
- config dev ide interp kernel lib library parsing pretyping proofs
+ config dev ide interp intf kernel lib library parsing pretyping proofs
scripts states tactics test-suite theories tools toplevel
are distributed under the terms of the GNU Lesser General Public License
diff --git a/Makefile.common b/Makefile.common
index 22b06a40e..d5b152432 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -72,7 +72,7 @@ SRCDIRS:=\
config tools tools/coqdoc scripts lib \
kernel kernel/byterun library proofs tactics \
pretyping interp toplevel/utils toplevel parsing \
- ide/utils ide \
+ intf ide/utils ide \
$(addprefix plugins/, \
omega romega micromega quote ring \
setoid_ring xml extraction fourier \
@@ -345,7 +345,7 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
OCAMLDOCDIR=dev/ocamldoc
-DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \
+DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
./pretyping/*.mli ./interp/*.mli \
./parsing/*.mli ./proofs/*.mli \
./tactics/*.mli ./toplevel/*.mli)
diff --git a/_tags b/_tags
index cf8319bd9..08dc9f1af 100644
--- a/_tags
+++ b/_tags
@@ -64,6 +64,7 @@
"ide": include
"ide/utils": include
"interp": include
+"intf": include
"kernel": include
"kernel/byterun": include
"lib": include
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 743205888..5358673ff 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -13,7 +13,7 @@ exec $OCAMLDEBUG \
-I $CAMLP4LIB \
-I $COQTOP \
-I $COQTOP/config \
- -I $COQTOP/lib -I $COQTOP/kernel \
+ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \
-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
-I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
diff --git a/dev/printers.mllib b/dev/printers.mllib
index f93d01daf..c1a95cdb2 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -137,6 +137,6 @@ Tactic_printer
Egrammar
Himsg
Cerrors
-Vernacexpr
+Locality
Vernacinterp
Top_printers
diff --git a/toplevel/vernacexpr.ml b/intf/vernacexpr.mli
index 95384c1c9..238400806 100644
--- a/toplevel/vernacexpr.ml
+++ b/intf/vernacexpr.mli
@@ -6,25 +6,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Compat
-open Errors
open Pp
-open Util
open Names
open Tacexpr
-open Extend
open Genarg
open Topconstr
open Decl_kinds
-open Ppextend
-open Declaremods
-
-(* Toplevel control exceptions *)
-exception Drop
-exception Quit
-
open Libnames
-open Nametab
+
+(** Vernac expressions, produced by the parser *)
type lident = identifier located
type lname = name located
@@ -179,7 +169,7 @@ type inductive_expr =
type one_inductive_expr =
lident * local_binder list * constr_expr option * constructor_expr list
-type module_ast_inl = module_ast annotated
+type module_ast_inl = module_ast Declaremods.annotated
type module_binder = bool option * lident list * module_ast_inl
type grammar_tactic_prod_item_expr =
@@ -187,10 +177,10 @@ type grammar_tactic_prod_item_expr =
| TacNonTerm of loc * string * (Names.identifier * string) option
type syntax_modifier =
- | SetItemLevel of string list * production_level
+ | SetItemLevel of string list * Extend.production_level
| SetLevel of int
- | SetAssoc of gram_assoc
- | SetEntryType of string * simple_constr_prod_entry_key
+ | SetAssoc of Compat.gram_assoc
+ | SetEntryType of string * Extend.simple_constr_prod_entry_key
| SetOnlyParsing
| SetFormat of string located
@@ -276,8 +266,8 @@ type vernac_expr =
(* Modules and Module Types *)
| VernacDeclareModule of bool option * lident *
module_binder list * module_ast_inl
- | VernacDefineModule of bool option * lident *
- module_binder list * module_ast_inl module_signature * module_ast_inl list
+ | VernacDefineModule of bool option * lident * module_binder list *
+ module_ast_inl Declaremods.module_signature * module_ast_inl list
| VernacDeclareModuleType of lident *
module_binder list * module_ast_inl list * module_ast_inl list
| VernacInclude of module_ast_inl list
@@ -315,7 +305,7 @@ type vernac_expr =
locality_flag * onlyparsing_flag
| VernacDeclareImplicits of locality_flag * reference or_by_notation *
(explicitation * bool * bool) list list
- | VernacArguments of locality_flag * reference or_by_notation *
+ | VernacArguments of locality_flag * reference or_by_notation *
((name * bool * (loc * string) option * bool * bool) list) list *
int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes
| `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
@@ -365,133 +355,3 @@ type vernac_expr =
| VernacExtend of string * raw_generic_argument list
and located_vernac_expr = loc * vernac_expr
-
-
-(** Categories of [vernac_expr] *)
-
-let rec strip_vernac = function
- | VernacTime c | VernacTimeout(_,c) | VernacFail c -> strip_vernac c
- | c -> c (* TODO: what about VernacList ? *)
-
-let rec is_navigation_vernac = function
- | VernacResetInitial
- | VernacResetName _
- | VernacBacktrack _
- | VernacBackTo _
- | VernacBack _ -> true
- | c -> is_deep_navigation_vernac c
-
-and is_deep_navigation_vernac = function
- | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
- | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
- | _ -> false
-
-(* Locating errors raised just after the dot is parsed but before the
- interpretation phase *)
-
-let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s)
-
-(**********************************************************************)
-(* Managing locality *)
-
-let locality_flag = ref None
-
-let local_of_bool = function true -> Local | false -> Global
-
-let check_locality () =
- match !locality_flag with
- | Some (loc,true) ->
- syntax_checking_error loc
- "This command does not support the \"Local\" prefix.";
- | Some (loc,false) ->
- syntax_checking_error loc
- "This command does not support the \"Global\" prefix."
- | None -> ()
-
-(** Extracting the locality flag *)
-
-(* Commands which supported an inlined Local flag *)
-
-let enforce_locality_full local =
- let local =
- match !locality_flag with
- | Some (_,false) when local ->
- error "Cannot be simultaneously Local and Global."
- | Some (_,true) when local ->
- error "Use only prefix \"Local\"."
- | None ->
- if local then begin
- Flags.if_warn
- Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix.");
- Some true
- end else
- None
- | Some (_,b) -> Some b in
- locality_flag := None;
- local
-
-(* Commands which did not supported an inlined Local flag (synonym of
- [enforce_locality_full false]) *)
-
-let use_locality_full () =
- let r = Option.map snd !locality_flag in
- locality_flag := None;
- r
-
-(** Positioning locality for commands supporting discharging and export
- outside of modules *)
-
-(* For commands whose default is to discharge and export:
- Global is the default and is neutral;
- Local in a section deactivates discharge,
- Local not in a section deactivates export *)
-
-let make_locality = function Some true -> true | _ -> false
-
-let use_locality () = make_locality (use_locality_full ())
-
-let use_locality_exp () = local_of_bool (use_locality ())
-
-let enforce_locality local = make_locality (enforce_locality_full local)
-
-let enforce_locality_exp local = local_of_bool (enforce_locality local)
-
-(* For commands whose default is not to discharge and not to export:
- Global forces discharge and export;
- Local is the default and is neutral *)
-
-let use_non_locality () =
- match use_locality_full () with Some false -> false | _ -> true
-
-(* For commands whose default is to not discharge but to export:
- Global in sections forces discharge, Global not in section is the default;
- Local in sections is the default, Local not in section forces non-export *)
-
-let make_section_locality =
- function Some b -> b | None -> Lib.sections_are_opened ()
-
-let use_section_locality () =
- make_section_locality (use_locality_full ())
-
-let enforce_section_locality local =
- make_section_locality (enforce_locality_full local)
-
-(** Positioning locality for commands supporting export but not discharge *)
-
-(* For commands whose default is to export (if not in section):
- Global in sections is forbidden, Global not in section is neutral;
- Local in sections is the default, Local not in section forces non-export *)
-
-let make_module_locality = function
- | Some false ->
- if Lib.sections_are_opened () then
- error "This command does not support the Global option in sections.";
- false
- | Some true -> true
- | None -> false
-
-let use_module_locality () =
- make_module_locality (use_locality_full ())
-
-let enforce_module_locality local =
- make_module_locality (enforce_locality_full local)
diff --git a/lib/errors.ml b/lib/errors.ml
index 1060a8efd..026198a98 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -35,6 +35,8 @@ let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
exception Error_in_file of string * (bool * string * loc) * exn
exception Timeout
+exception Drop
+exception Quit
let handle_stack = ref []
diff --git a/lib/errors.mli b/lib/errors.mli
index a863c5e30..d04ebb3fe 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -38,6 +38,8 @@ val invalid_arg_loc : loc * string -> 'a
val todo : string -> unit
exception Timeout
+exception Drop
+exception Quit
(** Like [Exc_located], but specifies the outermost file read, the
input buffer associated to the location of the error (or the module name
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 2f129637d..bf0e13e02 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -12,6 +12,7 @@ open Topconstr
open Glob_term
open Tacexpr
open Vernacexpr
+open Locality
open Pcoq
open Prim
open Tactic
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index f86fd0fec..8ec546ffd 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -117,7 +117,7 @@ VERNAC COMMAND EXTEND Admit_Obligations
VERNAC COMMAND EXTEND Set_Solver
| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
set_default_tactic
- (Vernacexpr.use_section_locality ())
+ (Locality.use_section_locality ())
(Tacinterp.glob_tactic t) ]
END
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 23e7e31bf..5f44a9e9c 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -13,6 +13,7 @@ open Util
open Vernac_
open Topconstr
open Vernacexpr
+open Locality
open Prim
open Constr
open Tok
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 320ca4eb0..f684b9a0d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,6 +15,7 @@ open Names
open Topconstr
open Extend
open Vernacexpr
+open Locality
open Pcoq
open Tactic
open Decl_kinds
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 0d7cd3649..39fd88506 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -71,7 +71,7 @@ Tacexpr
Tok
Lexer
Extend
-Vernacexpr
+Locality
Extrawit
Pcoq
Q_util
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 48bb87214..a5ee551a5 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -59,7 +59,7 @@ let (set_default_solver, default_solver, print_default_solver) =
VERNAC COMMAND EXTEND Firstorder_Set_Solver
| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
set_default_solver
- (Vernacexpr.use_section_locality ())
+ (Locality.use_section_locality ())
(Tacinterp.glob_tactic t) ]
END
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index fb9439d73..2700b2b7d 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -613,6 +613,6 @@ END
VERNAC COMMAND EXTEND HintCut
| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
let entry = HintsCutEntry p in
- Auto.add_hints (Vernacexpr.use_section_locality ())
+ Auto.add_hints (Locality.use_section_locality ())
(match dbnames with None -> ["core"] | Some l -> l) entry ]
END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 458c5bec6..88170d6dd 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1477,7 +1477,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
new_instance binders instance (Some (CRecord (dummy_loc,None,fields)))
- ~global:(not (Vernacexpr.use_section_locality ())) ~generalize:false None
+ ~global:(not (Locality.use_section_locality ())) ~generalize:false None
let declare_instance_refl global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
@@ -1496,7 +1496,7 @@ let declare_instance_trans global binders a aeq n lemma =
let declare_relation ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
- let global = not (Vernacexpr.use_section_locality ()) in
+ let global = not (Locality.use_section_locality ()) in
let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
in ignore(anew_instance global binders instance []);
match (refl,symm,trans) with
@@ -1754,16 +1754,16 @@ let add_morphism glob binders m s n =
VERNAC COMMAND EXTEND AddSetoid1
[ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
- [ add_setoid (not (Vernacexpr.use_section_locality ())) [] a aeq t n ]
+ [ add_setoid (not (Locality.use_section_locality ())) [] a aeq t n ]
| [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
- [ add_setoid (not (Vernacexpr.use_section_locality ())) binders a aeq t n ]
+ [ add_setoid (not (Locality.use_section_locality ())) binders a aeq t n ]
| [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
- [ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ]
+ [ add_morphism_infer (not (Locality.use_section_locality ())) m n ]
| [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
- [ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ]
+ [ add_morphism (not (Locality.use_section_locality ())) [] m s n ]
| [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ] ->
- [ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ]
+ [ add_morphism (not (Locality.use_section_locality ())) binders m s n ]
END
(** Bind to "rewrite" too *)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 292c288a8..cc3c7c18d 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -102,7 +102,7 @@ let coqide_cmd_checks (loc,ast) =
user_error "Debug mode not available within CoqIDE";
if is_known_option ast then
user_error "Use CoqIDE display menu instead";
- if is_navigation_vernac ast then
+ if Vernac.is_navigation_vernac ast then
user_error "Use CoqIDE navigation instead";
if is_undo ast then
msgerrnl (str "Warning: rather use CoqIDE navigation instead");
@@ -362,8 +362,8 @@ let eval_call c =
let () = flush !orig_stdout in
let () = pr_debug "Exiting gracefully." in
exit 0
- | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!"
- | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!"
+ | Errors.Drop -> None, "Drop is not allowed by coqide!"
+ | Errors.Quit -> None, "Quit is not allowed by coqide!"
| Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
| Error_in_file (_,_,inner) -> None, pr_exn inner
| Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
new file mode 100644
index 000000000..436250c92
--- /dev/null
+++ b/toplevel/locality.ml
@@ -0,0 +1,112 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** * Managing locality *)
+
+let locality_flag = ref None
+
+let local_of_bool = function
+ | true -> Decl_kinds.Local
+ | false -> Decl_kinds.Global
+
+let check_locality () =
+ match !locality_flag with
+ | Some (loc,b) ->
+ let s = if b then "Local" else "Global" in
+ Errors.user_err_loc
+ (loc,"",Pp.str ("This command does not support the \""^s^"\" prefix."))
+ | None -> ()
+
+(** Extracting the locality flag *)
+
+(* Commands which supported an inlined Local flag *)
+
+let enforce_locality_full local =
+ let local =
+ match !locality_flag with
+ | Some (_,false) when local ->
+ Errors.error "Cannot be simultaneously Local and Global."
+ | Some (_,true) when local ->
+ Errors.error "Use only prefix \"Local\"."
+ | None ->
+ if local then begin
+ Flags.if_warn
+ Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix.");
+ Some true
+ end else
+ None
+ | Some (_,b) -> Some b in
+ locality_flag := None;
+ local
+
+(* Commands which did not supported an inlined Local flag (synonym of
+ [enforce_locality_full false]) *)
+
+let use_locality_full () =
+ let r = Option.map snd !locality_flag in
+ locality_flag := None;
+ r
+
+(** Positioning locality for commands supporting discharging and export
+ outside of modules *)
+
+(* For commands whose default is to discharge and export:
+ Global is the default and is neutral;
+ Local in a section deactivates discharge,
+ Local not in a section deactivates export *)
+
+let make_locality = function Some true -> true | _ -> false
+
+let use_locality () = make_locality (use_locality_full ())
+
+let use_locality_exp () = local_of_bool (use_locality ())
+
+let enforce_locality local = make_locality (enforce_locality_full local)
+
+let enforce_locality_exp local = local_of_bool (enforce_locality local)
+
+(* For commands whose default is not to discharge and not to export:
+ Global forces discharge and export;
+ Local is the default and is neutral *)
+
+let use_non_locality () =
+ match use_locality_full () with Some false -> false | _ -> true
+
+(* For commands whose default is to not discharge but to export:
+ Global in sections forces discharge, Global not in section is the default;
+ Local in sections is the default, Local not in section forces non-export *)
+
+let make_section_locality =
+ function Some b -> b | None -> Lib.sections_are_opened ()
+
+let use_section_locality () =
+ make_section_locality (use_locality_full ())
+
+let enforce_section_locality local =
+ make_section_locality (enforce_locality_full local)
+
+(** Positioning locality for commands supporting export but not discharge *)
+
+(* For commands whose default is to export (if not in section):
+ Global in sections is forbidden, Global not in section is neutral;
+ Local in sections is the default, Local not in section forces non-export *)
+
+let make_module_locality = function
+ | Some false ->
+ if Lib.sections_are_opened () then
+ Errors.error
+ "This command does not support the Global option in sections.";
+ false
+ | Some true -> true
+ | None -> false
+
+let use_module_locality () =
+ make_module_locality (use_locality_full ())
+
+let enforce_module_locality local =
+ make_module_locality (enforce_locality_full local)
diff --git a/toplevel/locality.mli b/toplevel/locality.mli
new file mode 100644
index 000000000..5e8d45d87
--- /dev/null
+++ b/toplevel/locality.mli
@@ -0,0 +1,61 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** * Managing locality *)
+
+val locality_flag : (Pp.loc * bool) option ref
+val check_locality : unit -> unit
+
+(** * Extracting the locality flag *)
+
+(** Commands which supported an inlined Local flag *)
+
+val enforce_locality_full : bool -> bool option
+
+(** Commands which did not supported an inlined Local flag
+ (synonym of [enforce_locality_full false]) *)
+
+val use_locality_full : unit -> bool option
+
+(** * Positioning locality for commands supporting discharging and export
+ outside of modules *)
+
+(** For commands whose default is to discharge and export:
+ Global is the default and is neutral;
+ Local in a section deactivates discharge,
+ Local not in a section deactivates export *)
+
+val make_locality : bool option -> bool
+val use_locality : unit -> bool
+val use_locality_exp : unit -> Decl_kinds.locality
+val enforce_locality : bool -> bool
+val enforce_locality_exp : bool -> Decl_kinds.locality
+
+(** For commands whose default is not to discharge and not to export:
+ Global forces discharge and export;
+ Local is the default and is neutral *)
+
+val use_non_locality : unit -> bool
+
+(** For commands whose default is to not discharge but to export:
+ Global in sections forces discharge, Global not in section is the default;
+ Local in sections is the default, Local not in section forces non-export *)
+
+val make_section_locality : bool option -> bool
+val use_section_locality : unit -> bool
+val enforce_section_locality : bool -> bool
+
+(** * Positioning locality for commands supporting export but not discharge *)
+
+(** For commands whose default is to export (if not in section):
+ Global in sections is forbidden, Global not in section is neutral;
+ Local in sections is the default, Local not in section forces non-export *)
+
+val make_module_locality : bool option -> bool
+val use_module_locality : unit -> bool
+val enforce_module_locality : bool -> bool
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 6a06ba3dc..952f80aad 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -12,7 +12,6 @@ open Util
open Flags
open Cerrors
open Vernac
-open Vernacexpr
open Pcoq
open Compat
@@ -302,11 +301,11 @@ let print_toplevel_error exc =
match exc with
| End_of_input ->
msgerrnl (mt ()); pp_flush(); exit 0
- | Vernacexpr.Drop -> (* Last chance *)
- if Mltop.is_ocaml_top() then raise Vernacexpr.Drop;
+ | Errors.Drop -> (* Last chance *)
+ if Mltop.is_ocaml_top() then raise Errors.Drop;
(str"Error: There is no ML toplevel." ++ fnl ())
- | Vernacexpr.Quit ->
- raise Vernacexpr.Quit
+ | Errors.Quit ->
+ raise Errors.Quit
| _ ->
(if is_pervasive_exn exc then (mt ()) else locstrm) ++
Errors.print exc
@@ -372,9 +371,9 @@ let rec loop () =
reset_input_buffer stdin top_buffer;
while true do do_vernac() done
with
- | Vernacexpr.Drop -> ()
+ | Errors.Drop -> ()
| End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
- | Vernacexpr.Quit -> exit 0
+ | Errors.Quit -> exit 0
| e ->
msgerrnl (str"Anomaly. Please report.");
loop ()
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index d242036f7..43d15eb43 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,7 +1,7 @@
Himsg
Cerrors
Class
-Vernacexpr
+Locality
Metasyntax
Auto_ind_decl
Libtypes
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5cb404df7..32387e793 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,6 +27,21 @@ exception DuringCommandInterp of Pp.loc * exn
exception HasNotFailed
+(* The navigation vernac commands will be handled separately *)
+
+let rec is_navigation_vernac = function
+ | VernacResetInitial
+ | VernacResetName _
+ | VernacBacktrack _
+ | VernacBackTo _
+ | VernacBack _ -> true
+ | c -> is_deep_navigation_vernac c
+
+and is_deep_navigation_vernac = function
+ | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
+ | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
+ | _ -> false
+
(* Specifies which file is read. The intermediate file names are
discarded here. The Drop exception becomes an error. We forget
if the error ocurred during interpretation or not *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 9998fb19c..79ea1a4c5 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -44,3 +44,6 @@ val load_vernac : bool -> string -> unit
(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
val compile : bool -> string -> unit
+
+
+val is_navigation_vernac : Vernacexpr.vernac_expr -> bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4c12b4e7b..b6e625136 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1626,7 +1626,7 @@ let interp c =
Flags.program_cmd := false;
Obligations.set_program_mode isprogcmd;
try
- interp c; check_locality ();
+ interp c; Locality.check_locality ();
Flags.program_mode := mode
with e ->
Flags.program_mode := mode;
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index c8d6d87ff..4862419e2 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -14,7 +14,6 @@ open Libnames
open Himsg
open Proof_type
open Tacinterp
-open Vernacexpr
let disable_drop e =
if e <> Drop then e
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 02:41:16 +0000