diff options
| -rw-r--r-- | intf/vernacexpr.mli | 73 | ||||
| -rw-r--r-- | lib/flags.ml | 5 | ||||
| -rw-r--r-- | lib/flags.mli | 5 | ||||
| -rw-r--r-- | parsing/g_obligations.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 8 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 132 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 136 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 12 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 6 | ||||
| -rw-r--r-- | toplevel/locality.ml | 76 | ||||
| -rw-r--r-- | toplevel/locality.mli | 40 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 258 | ||||
| -rw-r--r-- | toplevel/vernacinterp.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacinterp.mli | 2 |
16 files changed, 416 insertions, 349 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 49467a393..b311b770d 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -121,18 +121,21 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) type opacity_flag = bool (* true = Opaque; false = Transparent *) -type locality_flag = bool (* true = Local; false = Global *) type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) type inductive_flag = Decl_kinds.recursivity_kind type infer_flag = bool (* true = try to Infer record; false = nothing *) -type full_locality_flag = bool option (* true = Local; false = Global *) type onlyparsing_flag = Flags.compat_version option (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version which this notation is trying to be compatible with *) +type locality_flag = bool (* true = Local *) +type obsolete_locality = bool +(* Some grammar entries use obsolete_locality. This bool is to be backward + * compatible. If the grammar is fixed removing deprecated syntax, this + * bool should go away too *) type option_value = Interface.option_value = | BoolValue of bool @@ -249,28 +252,33 @@ type vernac_expr = (* Syntax *) | VernacTacticNotation of - locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr - | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list) - | VernacOpenCloseScope of (locality_flag * bool * scope_name) + int * grammar_tactic_prod_item_expr list * raw_tactic_expr + | VernacSyntaxExtension of + obsolete_locality * (lstring * syntax_modifier list) + | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) | VernacDelimiters of scope_name * string | VernacBindScope of scope_name * reference or_by_notation list - | VernacInfix of locality_flag * (lstring * syntax_modifier list) * + | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of - locality_flag * constr_expr * (lstring * syntax_modifier list) * + obsolete_locality * constr_expr * (lstring * syntax_modifier list) * scope_name option (* Gallina *) - | VernacDefinition of definition_kind * lident * definition_expr + | VernacDefinition of + (locality option * definition_object_kind) * lident * definition_expr | VernacStartTheoremProof of theorem_kind * (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * bool | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list + | VernacAssumption of (locality option * assumption_object_kind) * + inline * simple_binder with_coercion list | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of locality * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of locality * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of + locality option * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of + locality option * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list @@ -281,15 +289,14 @@ type vernac_expr = export_flag option * lreference list | VernacImport of export_flag * lreference list | VernacCanonical of reference or_by_notation - | VernacCoercion of locality_flag * reference or_by_notation * + | VernacCoercion of obsolete_locality * reference or_by_notation * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of locality_flag * lident * + | VernacIdentityCoercion of obsolete_locality * lident * class_rawexpr * class_rawexpr (* Type classes *) | VernacInstance of bool * (* abstract instance *) - bool * (* global *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) constr_expr option * (* props *) @@ -297,8 +304,7 @@ type vernac_expr = | VernacContext of local_binder list - | VernacDeclareInstances of - bool (* global *) * reference list (* instance names *) + | VernacDeclareInstances of reference list (* instance names *) | VernacDeclareClass of reference (* inductive or definition name *) @@ -321,7 +327,7 @@ type vernac_expr = | VernacAddLoadPath of rec_flag * string * DirPath.t option | VernacRemoveLoadPath of string | VernacAddMLPath of rec_flag * string - | VernacDeclareMLModule of locality_flag * string list + | VernacDeclareMLModule of string list | VernacChdir of string option (* State management *) @@ -336,33 +342,34 @@ type vernac_expr = (* Commands *) | VernacDeclareTacticDefinition of - (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list) - | VernacCreateHintDb of locality_flag * string * bool - | VernacRemoveHints of locality_flag * string list * reference list - | VernacHints of locality_flag * string list * hints_expr + (rec_flag * (reference * bool * raw_tactic_expr) list) + | VernacCreateHintDb of string * bool + | VernacRemoveHints of string list * reference list + | VernacHints of obsolete_locality * string list * hints_expr | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) * - locality_flag * onlyparsing_flag - | VernacDeclareImplicits of locality_flag * reference or_by_notation * + obsolete_locality * onlyparsing_flag + | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list - | VernacArguments of locality_flag * reference or_by_notation * + | VernacArguments of reference or_by_notation * ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list * int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list - | VernacArgumentsScope of locality_flag * reference or_by_notation * + | VernacArgumentsScope of reference or_by_notation * scope_name option list | VernacReserve of simple_binder list - | VernacGeneralizable of locality_flag * (lident list) option - | VernacSetOpacity of - locality_flag * (Conv_oracle.level * reference or_by_notation list) list - | VernacUnsetOption of full_locality_flag * Goptions.option_name - | VernacSetOption of full_locality_flag * Goptions.option_name * option_value + | VernacGeneralizable of (lident list) option + | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) + | VernacSetStrategy of + (Conv_oracle.level * reference or_by_notation list) list + | VernacUnsetOption of Goptions.option_name + | VernacSetOption of Goptions.option_name * option_value | VernacAddOption of Goptions.option_name * option_ref_value list | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name | VernacCheckMayEval of raw_red_expr option * int option * constr_expr | VernacGlobalCheck of constr_expr - | VernacDeclareReduction of locality_flag * string * raw_red_expr + | VernacDeclareReduction of string * raw_red_expr | VernacPrint of printable | VernacSearch of searchable * search_restriction | VernacLocate of locatable @@ -393,4 +400,8 @@ type vernac_expr = (* For extension *) | VernacExtend of string * raw_generic_argument list + (* Flags *) + | VernacProgram of vernac_expr + | VernacLocal of bool * vernac_expr + and located_vernac_expr = Loc.t * vernac_expr diff --git a/lib/flags.ml b/lib/flags.ml index bd31b4024..6c67cb237 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -84,11 +84,6 @@ let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros -(** [program_cmd] indicates that the current command is a Program one. - [program_mode] tells that Program mode has been activated, either - globally via [Set Program] or locally via the Program command prefix. *) - -let program_cmd = ref false let program_mode = ref false let is_program_mode () = !program_mode diff --git a/lib/flags.mli b/lib/flags.mli index 6b26c50d9..6325d7cd4 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -52,11 +52,6 @@ val is_auto_intros : unit -> bool val make_term_color : bool -> unit val is_term_color : unit -> bool -(** [program_cmd] indicates that the current command is a Program one. - [program_mode] tells that Program mode has been activated, either - globally via [Set Program] or locally via the Program command prefix. *) - -val program_cmd : bool ref val program_mode : bool ref val is_program_mode : unit -> bool diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index 4c863ee67..20fe3af64 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -107,7 +107,7 @@ VERNAC COMMAND EXTEND Admit_Obligations VERNAC COMMAND EXTEND Set_Solver | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ set_default_tactic - (Locality.use_section_locality ()) + (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (Tacintern.glob_tactic t) ] END diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 194ed5926..3090fd7f3 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -83,17 +83,17 @@ GEXTEND Gram (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; id = IDENT ; b = [ "discriminated" -> true | -> false ] -> - VernacCreateHintDb (use_module_locality (), id, b) + VernacCreateHintDb (id, b) | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> - VernacRemoveHints (use_module_locality (), dbnames, ids) + VernacRemoveHints (dbnames, ids) | IDENT "Hint"; local = obsolete_locality; h = hint; dbnames = opt_hintbases -> - VernacHints (enforce_module_locality local,dbnames, h) + VernacHints (local,dbnames, h) (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural; dbnames = opt_hintbases -> - VernacHints (use_module_locality (),dbnames, + VernacHints (false,dbnames, HintsResolve (List.map (fun x -> (n, true, x)) lc)) ] ]; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5787186ad..56abf3e1c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -74,15 +74,18 @@ GEXTEND Gram [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v - | locality; v = vernac_aux -> v ] ] + | IDENT "Local"; v = vernac_aux -> VernacLocal (true, v) + | IDENT "Global"; v = vernac_aux -> VernacLocal (false, v) + | v = vernac_aux -> v ] + ] ; vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) - [ [ IDENT "Program"; g = gallina; "." -> Flags.program_cmd := true; g - | IDENT "Program"; g = gallina_ext; "." -> Flags.program_cmd := true; g - | g = gallina; "." -> Flags.program_cmd := false; g - | g = gallina_ext; "." -> Flags.program_cmd := false; g + [ [ IDENT "Program"; g = gallina; "." -> VernacProgram g + | IDENT "Program"; g = gallina_ext; "." -> VernacProgram g + | g = gallina; "." -> g + | g = gallina_ext; "." -> g | c = command; "." -> c | c = syntax; "." -> c | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l @@ -92,11 +95,6 @@ GEXTEND Gram vernac_aux: LAST [ [ prfcom = default_command_entry -> prfcom ] ] ; - locality: - [ [ IDENT "Local" -> locality_flag := Some (!@loc,true) - | IDENT "Global" -> locality_flag := Some (!@loc,false) - | -> locality_flag := None ] ] - ; noedit_mode: [ [ c = subgoal_command -> c None] ] ; @@ -162,7 +160,7 @@ GEXTEND Gram | d = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b) | IDENT "Let"; id = identref; b = def_body -> - VernacDefinition ((Discharge, Definition), id, b) + VernacDefinition ((Some Discharge, Definition), id, b) (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -170,13 +168,13 @@ GEXTEND Gram let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (f,false,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (use_locality_exp (), recs) + VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (Discharge, recs) + VernacFixpoint (Some Discharge, recs) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (use_locality_exp (), corecs) + VernacCoFixpoint (None, corecs) | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (Discharge, corecs) + VernacCoFixpoint (Some Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] @@ -201,25 +199,22 @@ GEXTEND Gram | IDENT "Property" -> Property ] ] ; def_token: - [ [ "Definition" -> - (use_locality_exp (), Definition) - | IDENT "Example" -> - (use_locality_exp (), Example) - | IDENT "SubClass" -> - (use_locality_exp (), SubClass) ] ] + [ [ "Definition" -> (None, Definition) + | IDENT "Example" -> (None, Example) + | IDENT "SubClass" -> (None, SubClass) ] ] ; assumption_token: - [ [ "Hypothesis" -> (Discharge, Logical) - | "Variable" -> (Discharge, Definitional) - | "Axiom" -> (use_locality_exp (), Logical) - | "Parameter" -> (use_locality_exp (), Definitional) - | IDENT "Conjecture" -> (use_locality_exp (), Conjectural) ] ] + [ [ "Hypothesis" -> (Some Discharge, Logical) + | "Variable" -> (Some Discharge, Definitional) + | "Axiom" -> (None, Logical) + | "Parameter" -> (None, Definitional) + | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> (Discharge, Logical) - | IDENT "Variables" -> (Discharge, Definitional) - | IDENT "Axioms" -> (use_locality_exp (), Logical) - | IDENT "Parameters" -> (use_locality_exp (), Definitional) ] ] + [ [ IDENT "Hypotheses" -> (Some Discharge, Logical) + | IDENT "Variables" -> (Some Discharge, Definitional) + | IDENT "Axioms" -> (None, Logical) + | IDENT "Parameters" -> (None, Definitional) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) @@ -522,12 +517,12 @@ GEXTEND Gram gallina_ext: [ [ (* Transparent and Opaque *) IDENT "Transparent"; l = LIST1 smart_global -> - VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l]) + VernacSetOpacity (Conv_oracle.transparent, l) | IDENT "Opaque"; l = LIST1 smart_global -> - VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l]) + VernacSetOpacity (Conv_oracle.Opaque, l) | IDENT "Strategy"; l = - LIST1 [ lev=strategy_level; "["; q=LIST1 smart_global; "]" -> (lev,q)] -> - VernacSetOpacity (use_locality (),l) + LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> (v,q)] -> + VernacSetStrategy l (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical (AN qid) @@ -537,33 +532,33 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Global,CanonicalStructure),(Loc.ghost,s),d) + ((Some Global,CanonicalStructure),(Loc.ghost,s),d) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((use_locality_exp (),Coercion),(Loc.ghost,s),d) + VernacDefinition ((None,Coercion),(Loc.ghost,s),d) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((enforce_locality_exp true,Coercion),(Loc.ghost,s),d) + VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (enforce_locality true, f, s, t) + VernacIdentityCoercion (true, f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (use_locality (), f, s, t) + VernacIdentityCoercion (false, f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (enforce_locality true, AN qid, s, t) + VernacCoercion (true, AN qid, s, t) | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (enforce_locality true, ByNotation ntn, s, t) + VernacCoercion (true, ByNotation ntn, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (use_locality (), AN qid, s, t) + VernacCoercion (false, AN qid, s, t) | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (use_locality (), ByNotation ntn, s, t) + VernacCoercion (false, ByNotation ntn, s, t) | IDENT "Context"; c = binders -> VernacContext c @@ -573,13 +568,12 @@ GEXTEND Gram pri = OPT [ "|"; i = natural -> i ] ; props = [ ":="; "{"; r = record_declaration; "}" -> Some r | ":="; c = lconstr -> Some c | -> None ] -> - VernacInstance (false, not (use_section_locality ()), - snd namesup, (fst namesup, expl, t), props, pri) + VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) | IDENT "Existing"; IDENT "Instance"; id = global -> - VernacDeclareInstances (not (use_section_locality ()), [id]) + VernacDeclareInstances [id] | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global -> - VernacDeclareInstances (not (use_section_locality ()), ids) + VernacDeclareInstances ids | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is @@ -623,14 +617,14 @@ GEXTEND Gram if List.mem `SimplNeverUnfold mods && List.mem `SimplDontExposeCase mods then err_incompat "simpl never" "simpl nomatch"; - VernacArguments (use_section_locality(), qid, impl, nargs, mods) + VernacArguments (qid, impl, nargs, mods) (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> Flags.if_verbose msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); - VernacArgumentsScope (use_section_locality (),qid,scl) + VernacArgumentsScope (qid,scl) (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; @@ -638,7 +632,7 @@ GEXTEND Gram List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> Flags.if_verbose msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); - VernacDeclareImplicits (use_section_locality (),qid,pos) + VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl @@ -652,7 +646,7 @@ GEXTEND Gram | IDENT "No"; IDENT "Variables" -> None | ["Variable" | IDENT "Variables"]; idl = LIST1 identref -> Some idl ] -> - VernacGeneralizable (use_non_locality (), gen) ] ] + VernacGeneralizable gen ] ] ; arguments_modifier: [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase] @@ -713,7 +707,7 @@ GEXTEND Gram command: [ [ IDENT "Ltac"; l = LIST1 tacdef_body SEP "with" -> - VernacDeclareTacticDefinition (use_module_locality (), true, l) + VernacDeclareTacticDefinition (true, l) | IDENT "Comments"; l = LIST0 comment -> VernacComments l @@ -721,9 +715,7 @@ GEXTEND Gram | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, not (use_section_locality ()), - snd namesup, (fst namesup, expl, t), - None, pri) + VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri) (* System directory *) | IDENT "Pwd" -> VernacChdir None @@ -738,7 +730,7 @@ GEXTEND Gram s = [ s = ne_string -> s | s = IDENT -> s ] -> VernacLoad (verbosely, s) | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> - VernacDeclareMLModule (use_locality (), l) + VernacDeclareMLModule l | IDENT "Locate"; l = locatable -> VernacLocate l @@ -793,11 +785,11 @@ GEXTEND Gram (* Pour intervenir sur les tables de paramčtres *) | "Set"; table = option_table; v = option_value -> - VernacSetOption (use_locality_full(),table,v) + VernacSetOption (table,v) | "Set"; table = option_table -> - VernacSetOption (use_locality_full(),table,BoolValue true) + VernacSetOption (table,BoolValue true) | IDENT "Unset"; table = option_table -> - VernacUnsetOption (use_locality_full(),table) + VernacUnsetOption table | IDENT "Print"; IDENT "Table"; table = option_table -> VernacPrintOption table @@ -951,16 +943,16 @@ GEXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - VernacSetOption (None,["Ltac";"Debug"], BoolValue true) + VernacSetOption (["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (None,["Ltac";"Debug"], BoolValue false) + VernacSetOption (["Ltac";"Debug"], BoolValue false) (* registration of a custom reduction *) | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; r = Tactic.red_expr -> - VernacDeclareReduction (use_locality(),s,r) + VernacDeclareReduction (s,r) ] ]; END @@ -973,10 +965,10 @@ GEXTEND Gram syntax: [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (enforce_section_locality local,true,sc) + VernacOpenCloseScope (local,(true,sc)) | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (enforce_section_locality local,false,sc) + VernacOpenCloseScope (local,(false,sc)) | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> VernacDelimiters (sc,key) @@ -988,31 +980,31 @@ GEXTEND Gram op = ne_lstring; ":="; p = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacInfix (enforce_module_locality local,(op,modl),p,sc) + VernacInfix (local,(op,modl),p,sc) | IDENT "Notation"; local = obsolete_locality; id = identref; idl = LIST0 ident; ":="; c = constr; b = only_parsing -> VernacSyntacticDefinition - (id,(idl,c),enforce_module_locality local,b) + (id,(idl,c),local,b) | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacNotation (enforce_module_locality local,c,(s,modl),sc) + VernacNotation (local,c,(s,modl),sc) | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; pil = LIST1 production_item; ":="; t = Tactic.tactic - -> VernacTacticNotation (use_module_locality(),n,pil,t) + -> VernacTacticNotation (n,pil,t) | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> Metasyntax.check_infix_modifiers l; let (loc,s) = s in - VernacSyntaxExtension (use_module_locality(),((loc,"x '"^s^"' y"),l)) + VernacSyntaxExtension (false,((loc,"x '"^s^"' y"),l)) | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (enforce_module_locality local,(s,l)) + -> VernacSyntaxExtension (local,(s,l)) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 0cb45f51d..bdea8b1a9 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -56,7 +56,7 @@ let (set_default_solver, default_solver, print_default_solver) = VERNAC COMMAND EXTEND Firstorder_Set_Solver | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ set_default_solver - (Locality.use_section_locality ()) + (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (Tacintern.glob_tactic t) ] END diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 572876e5b..415d70316 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -177,7 +177,7 @@ let pr_reference_or_constr pr_c = function | HintsReference r -> pr_reference r | HintsConstr c -> pr_c c -let pr_hints local db h pr_c pr_pat = +let pr_hints db h pr_c pr_pat = let opth = pr_opt_hintbases db in let pph = match h with @@ -200,7 +200,7 @@ let pr_hints local db h pr_c pr_pat = str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ spc() ++ pr_raw_tactic tac in - hov 2 (str"Hint "++pr_locality local ++ pph ++ opth) + hov 2 (str"Hint "++ pph ++ opth) let pr_with_declaration pr_c = function | CWith_Definition (id,c) -> @@ -306,7 +306,9 @@ let pr_class_rawexpr = function | SortClass -> str"Sortclass" | RefClass qid -> pr_smart_global qid -let pr_assumption_token many = function +let pr_assumption_token many (l,a) = + let l = match l with Some x -> x | None -> Decl_kinds.Global in + match l, a with | (Discharge,Logical) -> str (if many then "Hypotheses" else "Hypothesis") | (Discharge,Definitional) -> @@ -475,6 +477,8 @@ let pr_printable = function in let rec pr_vernac = function + | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v + | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v (* Proof management *) | VernacAbortAll -> str "Abort All" @@ -530,10 +534,9 @@ let rec pr_vernac = function | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v (* Syntax *) - | VernacTacticNotation (local,n,r,e) -> - pr_locality local ++ pr_grammar_tactic_rule n ("",r,e) - | VernacOpenCloseScope (local,opening,sc) -> - pr_section_locality local ++ + | VernacTacticNotation (n,r,e) -> + pr_grammar_tactic_rule n ("",r,e) + | VernacOpenCloseScope (_,(opening,sc)) -> str (if opening then "Open " else "Close ") ++ str "Scope" ++ spc() ++ str sc | VernacDelimiters (sc,key) -> @@ -542,20 +545,20 @@ let rec pr_vernac = function | VernacBindScope (sc,cll) -> str"Bind Scope" ++ spc () ++ str sc ++ spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll - | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function + | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function | None -> str"_" | Some sc -> str sc in - pr_section_locality local ++ str"Arguments Scope" ++ spc() ++ + str"Arguments Scope" ++ spc() ++ pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - | VernacInfix (local,((_,s),mv),q,sn) -> (* A Verifier *) - hov 0 (hov 0 (pr_locality local ++ str"Infix " + | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *) + hov 0 (hov 0 (str"Infix " ++ qs s ++ str " :=" ++ pr_constrarg q) ++ pr_syntax_modifiers mv ++ (match sn with | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) - | VernacNotation (local,c,((_,s),l),opt) -> + | VernacNotation (_,c,((_,s),l),opt) -> let ps = let n = String.length s in if n > 2 && s.[0] == '\'' && s.[n-1] == '\'' @@ -563,18 +566,20 @@ let rec pr_vernac = function let s' = String.sub s 1 (n-2) in if String.contains s' '\'' then qs s else str s' else qs s in - hov 2 (pr_locality local ++ str"Notation" ++ spc() ++ ps ++ + hov 2 (str"Notation" ++ spc() ++ ps ++ str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++ (match opt with | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) - | VernacSyntaxExtension (local,(s,l)) -> - pr_locality local ++ str"Reserved Notation" ++ spc() ++ pr_located qs s ++ + | VernacSyntaxExtension (_,(s,l)) -> + str"Reserved Notation" ++ spc() ++ pr_located qs s ++ pr_syntax_modifiers l (* Gallina *) | VernacDefinition (d,id,b) -> (* A verifier... *) - let pr_def_token dk = str (Kindops.string_of_definition_kind dk) in + let pr_def_token (l,dk) = + let l = match l with Some x -> x | None -> Decl_kinds.Global in + str (Kindops.string_of_definition_kind (l,dk)) in let pr_reduce = function | None -> mt() | Some r -> @@ -650,9 +655,9 @@ let rec pr_vernac = function | VernacFixpoint (local, recs) -> let local = match local with - | Discharge -> "Let " - | Local -> "Local " - | Global -> "" + | Some Discharge -> "Let " + | Some Local -> "Local " + | None | Some Global -> "" in let pr_onerec = function | ((loc,id),ro,bl,type_,def),ntn -> @@ -667,9 +672,9 @@ let rec pr_vernac = function | VernacCoFixpoint (local, corecs) -> let local = match local with - | Discharge -> "Let " - | Local -> "Local " - | Global -> "" + | Some Discharge -> "Let " + | Some Local -> "Local " + | None | Some Global -> "" in let pr_onecorec (((loc,id),bl,c,def),ntn) = pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ @@ -698,22 +703,19 @@ let rec pr_vernac = function (if f then str"Export" else str"Import") ++ spc() ++ prlist_with_sep sep pr_import_module l | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q - | VernacCoercion (s,id,c1,c2) -> + | VernacCoercion (_,id,c1,c2) -> hov 1 ( - str"Coercion" ++ (if s then spc() ++ - str"Local" ++ spc() else spc()) ++ + str"Coercion" ++ pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) - | VernacIdentityCoercion (s,id,c1,c2) -> + | VernacIdentityCoercion (_,id,c1,c2) -> hov 1 ( - str"Identity Coercion" ++ (if s then spc() ++ - str"Local" ++ spc() else spc()) ++ pr_lident id ++ + str"Identity Coercion" ++ pr_lident id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) - | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) -> + | VernacInstance (abst, sup, (instid, bk, cl), props, pri) -> hov 1 ( - pr_non_locality (not glob) ++ (if abst then str"Declare " else mt ()) ++ str"Instance" ++ (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | @@ -730,10 +732,10 @@ let rec pr_vernac = function str"Context" ++ spc () ++ pr_and_type_binders_arg l) - | VernacDeclareInstances (glob, ids) -> - hov 1 (pr_non_locality (not glob) ++ - str"Existing" ++ spc () ++ str(String.plural (List.length ids) "Instance") ++ - spc () ++ prlist_with_sep spc pr_reference ids) + | VernacDeclareInstances ids -> + hov 1 ( str"Existing" ++ spc () ++ + str(String.plural (List.length ids) "Instance") ++ + spc () ++ prlist_with_sep spc pr_reference ids) | VernacDeclareClass id -> hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id) @@ -784,13 +786,12 @@ let rec pr_vernac = function | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s | VernacAddMLPath (fl,s) -> str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s - | VernacDeclareMLModule (local, l) -> - pr_locality local ++ + | VernacDeclareMLModule (l) -> hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l) | VernacChdir s -> str"Cd" ++ pr_opt qs s (* Commands *) - | VernacDeclareTacticDefinition (local,rc,l) -> + | VernacDeclareTacticDefinition (rc,l) -> let pr_tac_body (id, redef, body) = let idl, body = match body with @@ -803,34 +804,33 @@ let rec pr_vernac = function pr_raw_tactic body in hov 1 - (pr_locality local ++ str "Ltac " ++ + (str "Ltac " ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) - | VernacCreateHintDb (local,dbname,b) -> - hov 1 (pr_locality local ++ str "Create HintDb " ++ + | VernacCreateHintDb (dbname,b) -> + hov 1 (str "Create HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ())) - | VernacRemoveHints (local, dbnames, ids) -> - hov 1 (pr_locality local ++ str "Remove Hints " ++ + | VernacRemoveHints (dbnames, ids) -> + hov 1 (str "Remove Hints " ++ prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ pr_opt_hintbases dbnames) - | VernacHints (local,dbnames,h) -> - pr_hints local dbnames h pr_constr pr_constr_pattern_expr - | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> + | VernacHints (_, dbnames,h) -> + pr_hints dbnames h pr_constr pr_constr_pattern_expr + | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> hov 2 - (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++ + (str"Notation " ++ pr_lident id ++ spc () ++ prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) - | VernacDeclareImplicits (local,q,[]) -> - hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ - pr_smart_global q) - | VernacDeclareImplicits (local,q,impls) -> - hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ + | VernacDeclareImplicits (q,[]) -> + hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q) + | VernacDeclareImplicits (q,impls) -> + hov 1 (str"Implicit Arguments " ++ spc() ++ pr_smart_global q ++ spc() ++ prlist_with_sep spc (fun imps -> str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") impls) - | VernacArguments (local, q, impl, nargs, mods) -> - hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++ + | VernacArguments (q, impl, nargs, mods) -> + hov 2 (str"Arguments" ++ spc() ++ pr_smart_global q ++ let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in let pr_if b x = if b then x else str "" in @@ -861,21 +861,23 @@ let rec pr_vernac = function hov 2 (str"Implicit Type" ++ str (if n > 1 then "s " else " ") ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl)) - | VernacGeneralizable (local, g) -> - hov 1 (pr_locality local ++ str"Generalizable Variable" ++ + | VernacGeneralizable g -> + hov 1 (str"Generalizable Variable" ++ match g with | None -> str "s none" | Some [] -> str "s all" | Some idl -> str (if List.length idl > 1 then "s " else " ") ++ prlist_with_sep spc pr_lident idl) - | VernacSetOpacity(b,[k,l]) when Conv_oracle.is_transparent k -> - hov 1 (pr_non_locality b ++ str "Transparent" ++ + | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k -> + hov 1 (str "Transparent" ++ spc() ++ prlist_with_sep sep pr_smart_global l) - | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) -> - hov 1 (pr_non_locality b ++ str "Opaque" ++ + | VernacSetOpacity(Conv_oracle.Opaque,l) -> + hov 1 (str "Opaque" ++ spc() ++ prlist_with_sep sep pr_smart_global l) - | VernacSetOpacity (local,l) -> + | VernacSetOpacity _ -> + Errors.anomaly (str "VernacSetOpacity used to set something else") + | VernacSetStrategy l -> let pr_lev = function Conv_oracle.Opaque -> str"opaque" | Conv_oracle.Expand -> str"expand" @@ -884,12 +886,12 @@ let rec pr_vernac = function let pr_line (l,q) = hov 2 (pr_lev l ++ spc() ++ str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in - hov 1 (pr_locality local ++ str "Strategy" ++ spc() ++ + hov 1 (str "Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) - | VernacUnsetOption (l,na) -> - hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None) - | VernacSetOption (l,na,v) -> - hov 2 (pr_locality_full l ++ str"Set" ++ spc() ++ pr_set_option na v) + | VernacUnsetOption (na) -> + hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) + | VernacSetOption (na,v) -> + hov 2 (str"Set" ++ spc() ++ pr_set_option na v) | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l)) | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l)) | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l)) @@ -905,8 +907,8 @@ let rec pr_vernac = function let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in pr_i ++ pr_mayeval r c | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c) - | VernacDeclareReduction (b,s,r) -> - pr_locality b ++ str "Declare Reduction " ++ str s ++ str " := " ++ + | VernacDeclareReduction (s,r) -> + str "Declare Reduction " ++ str s ++ str " := " ++ pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r | VernacPrint p -> pr_printable p | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 1be29aefe..713d6f233 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -603,6 +603,6 @@ END VERNAC COMMAND EXTEND HintCut | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ let entry = HintsCutEntry p in - Auto.add_hints (Locality.use_section_locality ()) + Auto.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (match dbnames with None -> ["core"] | Some l -> l) entry ] END diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index ad8517c32..dc59005f6 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1606,7 +1606,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 (Locality.use_section_locality ()) in + let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) 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 @@ -1864,16 +1864,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 (Locality.use_section_locality ())) [] a aeq t n ] + [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.use_section_locality ())) binders a aeq t n ] + [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> - [ add_morphism_infer (not (Locality.use_section_locality ())) m n ] + [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Locality.use_section_locality ())) [] m s n ] + [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Locality.use_section_locality ())) binders m s n ] + [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] END (** Bind to "rewrite" too *) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 6e7ed6e7f..681f0f2c8 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -74,12 +74,12 @@ let coqide_known_option table = List.mem table [ ["Printing";"Universes"]] let is_known_option cmd = match cmd with - | VernacSetOption (_,o,BoolValue true) - | VernacUnsetOption (_,o) -> coqide_known_option o + | VernacSetOption (o,BoolValue true) + | VernacUnsetOption o -> coqide_known_option o | _ -> false let is_debug cmd = match cmd with - | VernacSetOption (_,["Ltac";"Debug"], _) -> true + | VernacSetOption (["Ltac";"Debug"], _) -> true | _ -> false let is_query cmd = match cmd with diff --git a/toplevel/locality.ml b/toplevel/locality.ml index 88c3b3c05..49478cb26 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -8,30 +8,27 @@ (** * 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 check_locality locality_flag = + match locality_flag with + | Some 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.")) + Errors.error ("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 enforce_locality_full locality_flag local = let local = - match !locality_flag with - | Some (_,false) when local -> + match locality_flag with + | Some false when local -> Errors.error "Cannot be simultaneously Local and Global." - | Some (_,true) when local -> + | Some true when local -> Errors.error "Use only prefix \"Local\"." | None -> if local then begin @@ -40,18 +37,9 @@ let enforce_locality_full local = Some true end else None - | Some (_,b) -> Some b in - locality_flag := None; + | Some b -> Some b in 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 *) @@ -59,23 +47,19 @@ let use_locality_full () = Global is the default and is neutral; Local in a section deactivates discharge, Local not in a section deactivates export *) +let make_non_locality = function Some false -> false | _ -> true 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 locality_flag local = + make_locality (enforce_locality_full locality_flag 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 +let enforce_locality_exp locality_flag local = + match locality_flag, local with + | None, Some local -> local + | Some b, None -> local_of_bool b + | None, None -> Decl_kinds.Global + | Some _, Some _ -> Errors.error "Local non allowed in this case" (* For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; @@ -84,11 +68,8 @@ let use_non_locality () = 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) +let enforce_section_locality locality_flag local = + make_section_locality (enforce_locality_full locality_flag local) (** Positioning locality for commands supporting export but not discharge *) @@ -105,8 +86,15 @@ let make_module_locality = function | 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) +let enforce_module_locality locality_flag local = + make_module_locality (enforce_locality_full locality_flag local) + +module LocalityFixme = struct + let locality = ref None + let set l = locality := l + let consume () = + let l = !locality in + locality := None; + l + let assert_consumed () = check_locality !locality +end diff --git a/toplevel/locality.mli b/toplevel/locality.mli index b63378ed1..d98c9fa88 100644 --- a/toplevel/locality.mli +++ b/toplevel/locality.mli @@ -8,19 +8,9 @@ (** * Managing locality *) -val locality_flag : (Loc.t * 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 +val enforce_locality_full : bool option -> bool -> bool option (** * Positioning locality for commands supporting discharging and export outside of modules *) @@ -31,24 +21,17 @@ val use_locality_full : unit -> bool option 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 +val make_non_locality : bool option -> bool +val enforce_locality : bool option -> bool -> bool +val enforce_locality_exp : + bool option -> Decl_kinds.locality option -> Decl_kinds.locality (** 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 +val enforce_section_locality : bool option -> bool -> bool (** * Positioning locality for commands supporting export but not discharge *) @@ -57,5 +40,12 @@ val enforce_section_locality : bool -> bool 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 +val enforce_module_locality : bool option -> bool -> bool + +(* This is the old imperative interface that is still used for + * VernacExtend vernaculars. Time permitting this could be trashed too *) +module LocalityFixme : sig + val set : bool option -> unit + val consume : unit -> bool option + val assert_consumed : unit -> unit +end diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d713fdcc2..a3aa6607e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -32,6 +32,7 @@ open Redexpr open Lemmas open Declaremods open Misctypes +open Locality (* Misc *) @@ -433,27 +434,35 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension = Metasyntax.add_syntax_extension +let vernac_syntax_extension locality local = + let local = enforce_module_locality locality local in + Metasyntax.add_syntax_extension local let vernac_delimiters = Metasyntax.add_delimiters let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) -let vernac_open_close_scope = Notation.open_close_scope +let vernac_open_close_scope locality local (b,s) = + let local = enforce_section_locality locality local in + Notation.open_close_scope (local,b,s) -let vernac_arguments_scope local r scl = +let vernac_arguments_scope locality r scl = + let local = make_section_locality locality in Notation.declare_arguments_scope local (smart_global r) scl -let vernac_infix = Metasyntax.add_infix +let vernac_infix locality local = + let local = enforce_module_locality locality local in + Metasyntax.add_infix local -let vernac_notation = Metasyntax.add_notation +let vernac_notation locality local = + let local = enforce_module_locality locality local in + Metasyntax.add_notation local (***********) (* Gallina *) let start_proof_and_print k l hook = - Locality.check_locality (); (* early check, cf #2975 *) start_proof_com k l hook; print_subgoals () @@ -465,7 +474,8 @@ let vernac_definition_hook = function | SubClass -> Class.add_subclass_hook | _ -> no_hook -let vernac_definition (local,k) (loc,id as lid) def = +let vernac_definition locality (local,k) (loc,id as lid) def = + let local = enforce_locality_exp locality local in let hook = vernac_definition_hook k in let () = match local with | Discharge -> Dumpglob.dump_definition lid true "var" @@ -523,8 +533,10 @@ let vernac_exact_proof c = save_named true; Backtrack.mark_unreachable [prf] -let vernac_assumption kind l nl= - let global = (fst kind) == Global in +let vernac_assumption locality (local, kind) l nl= + let local = enforce_locality_exp locality local in + let global = local == Global in + let kind = local, kind in let status = List.fold_left (fun status (is_coe,(idl,c)) -> if Dumpglob.dump () then @@ -582,12 +594,14 @@ let vernac_inductive finite infer indl = let indl = List.map unpack indl in do_mutual_inductive indl (finite != CoFinite) -let vernac_fixpoint local l = +let vernac_fixpoint locality local l = + let local = enforce_locality_exp locality local in if Dumpglob.dump () then List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_fixpoint local l -let vernac_cofixpoint local l = +let vernac_cofixpoint locality local l = + let local = enforce_locality_exp locality local in if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_cofixpoint local l @@ -774,28 +788,32 @@ let vernac_require import qidl = let vernac_canonical r = Recordops.declare_canonical_structure (smart_global r) -let vernac_coercion stre ref qids qidt = +let vernac_coercion locality local ref qids qidt = + let local = enforce_locality locality local in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' ~local:stre ~source ~target; + Class.try_add_new_coercion_with_target ref' ~local ~source ~target; if_verbose msg_info (pr_global ref' ++ str " is now a coercion") -let vernac_identity_coercion stre id qids qidt = +let vernac_identity_coercion locality local id qids qidt = + let local = enforce_locality locality local in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - Class.try_add_new_identity_coercion id ~local:stre ~source ~target + Class.try_add_new_identity_coercion id ~local ~source ~target (* Type classes *) -let vernac_instance abst glob sup inst props pri = +let vernac_instance abst locality sup inst props pri = + let glob = not (make_section_locality locality) in Dumpglob.dump_constraint inst false "inst"; ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri) let vernac_context l = if not (Classes.context l) then raise UnsafeSuccess -let vernac_declare_instances glob ids = +let vernac_declare_instances locality ids = + let glob = not (make_section_locality locality) in List.iter (fun (id) -> Classes.existing_instance glob id) ids let vernac_declare_class id = @@ -870,7 +888,8 @@ let vernac_remove_loadpath path = let vernac_add_ml_path isrec path = (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path) -let vernac_declare_ml_module local l = +let vernac_declare_ml_module locality l = + let local = make_locality locality in Mltop.declare_ml_modules local (List.map expand l) let vernac_chdir = function @@ -897,30 +916,37 @@ let vernac_restore_state file = (************) (* Commands *) -let vernac_declare_tactic_definition (local,x,def) = +let vernac_declare_tactic_definition locality (x,def) = + let local = make_module_locality locality in Tacintern.add_tacdef local x def -let vernac_create_hintdb local id b = +let vernac_create_hintdb locality id b = + let local = make_module_locality locality in Auto.create_hint_db local id full_transparent_state b -let vernac_remove_hints local dbs ids = +let vernac_remove_hints locality dbs ids = + let local = make_module_locality locality in Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids) -let vernac_hints local lb h = +let vernac_hints locality local lb h = + let local = enforce_module_locality locality local in Auto.add_hints local lb (Auto.interp_hints h) -let vernac_syntactic_definition lid = +let vernac_syntactic_definition locality lid x local y = Dumpglob.dump_definition lid false "syndef"; - Metasyntax.add_syntactic_definition (snd lid) + let local = enforce_module_locality locality local in + Metasyntax.add_syntactic_definition (snd lid) x local y -let vernac_declare_implicits local r = function +let vernac_declare_implicits locality r l = + let local = make_section_locality locality in + match l with | [] -> Impargs.declare_implicits local (smart_global r) | _::_ as imps -> Impargs.declare_manual_implicits local (smart_global r) ~enriching:false (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps) -let vernac_declare_arguments local r l nargs flags = +let vernac_declare_arguments locality r l nargs flags = let extra_scope_flag = List.mem `ExtraScopes flags in let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in let names, rest = List.hd names, List.tl names in @@ -989,7 +1015,9 @@ let vernac_declare_arguments local r l nargs flags = if some_renaming_specified then if not (List.mem `Rename flags) then error "To rename arguments the \"rename\" flag must be specified." - else Arguments_renaming.rename_arguments local sr names_decl; + else + Arguments_renaming.rename_arguments + (make_section_locality locality) sr names_decl; (* All other infos are in the first item of l *) let l = List.hd l in let some_implicits_specified = match implicits with @@ -1006,11 +1034,11 @@ let vernac_declare_arguments local r l nargs flags = Util.List.map_filter (function (n, true) -> Some n | _ -> None) (Util.List.map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in if some_scopes_specified || List.mem `ClearScopes flags then - vernac_arguments_scope local r scopes; + vernac_arguments_scope locality r scopes; if not some_implicits_specified && List.mem `DefaultImplicits flags then - vernac_declare_implicits local r [] + vernac_declare_implicits locality r [] else if some_implicits_specified || List.mem `ClearImplicits flags then - vernac_declare_implicits local r implicits; + vernac_declare_implicits locality r implicits; if nargs >= 0 && nargs < List.fold_left max 0 rargs then error "The \"/\" option must be placed after the last \"!\"."; let rec narrow = function @@ -1020,7 +1048,8 @@ let vernac_declare_arguments local r l nargs flags = if not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) then match sr with | ConstRef _ as c -> - Tacred.set_simpl_behaviour local c (rargs, nargs, flags) + Tacred.set_simpl_behaviour + (make_section_locality locality) c (rargs, nargs, flags) | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.") let vernac_reserve bl = @@ -1031,7 +1060,9 @@ let vernac_reserve bl = Reserve.declare_reserved_type idl t) in List.iter sb_decl bl -let vernac_generalizable = Implicit_quantifiers.declare_generalizable +let vernac_generalizable locality = + let local = make_non_locality locality in + Implicit_quantifiers.declare_generalizable local let _ = declare_bool_option @@ -1284,15 +1315,27 @@ let _ = optread = (fun () -> !Constrintern.parsing_explicit); optwrite = (fun b -> Constrintern.parsing_explicit := b) } -let vernac_set_opacity local str = +let vernac_set_strategy locality l = + let local = make_locality locality in let glob_ref r = match smart_global r with | ConstRef sp -> EvalConstRef sp | VarRef id -> EvalVarRef id | _ -> error "cannot set an inductive type or a constructor as transparent" in - let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in - Redexpr.set_strategy local str + let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in + Redexpr.set_strategy local l + +let vernac_set_opacity locality (v,l) = + let local = make_non_locality locality in + let glob_ref r = + match smart_global r with + | ConstRef sp -> EvalConstRef sp + | VarRef id -> EvalVarRef id + | _ -> error + "cannot set an inductive type or a constructor as transparent" in + let l = List.map glob_ref l in + Redexpr.set_strategy local [v,l] let vernac_set_option locality key = function | StringValue s -> set_string_option_value_gen locality key s @@ -1356,7 +1399,8 @@ let vernac_check_may_eval redexp glopt rc = msg_notice (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = - declare_red_expr locality s (snd (interp_redexp (Global.env()) Evd.empty r)) + let local = make_locality locality in + declare_red_expr local s (snd (interp_redexp (Global.env()) Evd.empty r)) (* The same but avoiding the current goal context if any *) let vernac_global_check c = @@ -1670,30 +1714,36 @@ let vernac_check_guard () = in msg_notice message -let interp c = match c with +(* "locality" is the prefix "Local" attribute, while the "local" component + * is the outdated/deprecated "Local" attribute of some vernacular commands + * still parsed as the obsolete_locality grammar entry for retrocompatibility *) +let interp locality c = match c with (* Control (done in vernac) *) | (VernacTime _|VernacList _|VernacLoad _|VernacTimeout _|VernacFail _) -> assert false (* Syntax *) - | VernacTacticNotation (b,n,r,e) -> Metasyntax.add_tactic_notation (b,n,r,e) - | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl + | VernacTacticNotation (n,r,e) -> + Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e) + | VernacSyntaxExtension (local,sl) -> + vernac_syntax_extension locality local sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl - | VernacOpenCloseScope sc -> vernac_open_close_scope sc - | VernacArgumentsScope (lcl,qid,scl) -> vernac_arguments_scope lcl qid scl - | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc - | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc + | VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s + | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope locality qid scl + | VernacInfix (local,mv,qid,sc) -> vernac_infix locality local mv qid sc + | VernacNotation (local,c,infpl,sc) -> + vernac_notation locality local c infpl sc (* Gallina *) - | VernacDefinition (k,lid,d) -> vernac_definition k lid d + | VernacDefinition (k,lid,d) -> vernac_definition locality k lid d | VernacStartTheoremProof (k,l,top) -> vernac_start_proof k l top | VernacEndProof e -> vernac_end_proof e | VernacExactProof c -> vernac_exact_proof c - | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl + | VernacAssumption (stre,nl,l) -> vernac_assumption locality stre l nl | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l - | VernacFixpoint (local, l) -> vernac_fixpoint local l - | VernacCoFixpoint (local, l) -> vernac_cofixpoint local l + | VernacFixpoint (local, l) -> vernac_fixpoint locality local l + | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l @@ -1714,14 +1764,15 @@ let interp c = match c with | VernacRequire (export, qidl) -> vernac_require export qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid - | VernacCoercion (str,r,s,t) -> vernac_coercion str r s t - | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t + | VernacCoercion (local,r,s,t) -> vernac_coercion locality local r s t + | VernacIdentityCoercion (local,(_,id),s,t) -> + vernac_identity_coercion locality local id s t (* Type classes *) - | VernacInstance (abst, glob, sup, inst, props, pri) -> - vernac_instance abst glob sup inst props pri + | VernacInstance (abst, sup, inst, props, pri) -> + vernac_instance abst locality sup inst props pri | VernacContext sup -> vernac_context sup - | VernacDeclareInstances (glob, ids) -> vernac_declare_instances glob ids + | VernacDeclareInstances ids -> vernac_declare_instances locality ids | VernacDeclareClass id -> vernac_declare_class id (* Solving *) @@ -1733,7 +1784,7 @@ let interp c = match c with | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias | VernacRemoveLoadPath s -> vernac_remove_loadpath s | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s - | VernacDeclareMLModule (local, l) -> vernac_declare_ml_module local l + | VernacDeclareMLModule l -> vernac_declare_ml_module locality l | VernacChdir s -> vernac_chdir s (* State management *) @@ -1747,24 +1798,30 @@ let interp c = match c with | VernacBackTo n -> vernac_backto n (* Commands *) - | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def - | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b - | VernacRemoveHints (local,dbnames,ids) -> vernac_remove_hints local dbnames ids - | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints - | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b - | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l - | VernacArguments (local, qid, l, narg, flags) -> vernac_declare_arguments local qid l narg flags + | VernacDeclareTacticDefinition def -> + vernac_declare_tactic_definition locality def + | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b + | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids + | VernacHints (local,dbnames,hints) -> + vernac_hints locality local dbnames hints + | VernacSyntacticDefinition (id,c,local,b) -> + vernac_syntactic_definition locality id c local b + | VernacDeclareImplicits (qid,l) -> + vernac_declare_implicits locality qid l + | VernacArguments (qid, l, narg, flags) -> + vernac_declare_arguments locality qid l narg flags | VernacReserve bl -> vernac_reserve bl - | VernacGeneralizable (local,gen) -> vernac_generalizable local gen - | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl - | VernacSetOption (locality,key,v) -> vernac_set_option locality key v - | VernacUnsetOption (locality,key) -> vernac_unset_option locality key + | VernacGeneralizable gen -> vernac_generalizable locality gen + | VernacSetOpacity qidl -> vernac_set_opacity locality qidl + | VernacSetStrategy l -> vernac_set_strategy locality l + | VernacSetOption (key,v) -> vernac_set_option locality key v + | VernacUnsetOption key -> vernac_unset_option locality key | VernacRemoveOption (key,v) -> vernac_remove_option key v | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c - | VernacDeclareReduction (b,s,r) -> vernac_declare_reduction b s r + | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r | VernacGlobalCheck c -> vernac_global_check c | VernacPrint p -> vernac_print p | VernacSearch (s,r) -> vernac_search s r @@ -1798,23 +1855,58 @@ let interp c = match c with | VernacToplevelControl e -> raise e (* Extensions *) - | VernacExtend (opn,args) -> Vernacinterp.call (opn,args) + | VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args) + + (* Handled elsewhere *) + | VernacProgram _ + | VernacLocal _ -> assert false + +(* Vernaculars that take a locality flag *) +let check_vernac_supports_locality c l = + match l, c with + | None, _ -> () + | Some _, ( + VernacTacticNotation _ + | VernacOpenCloseScope _ + | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ + | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ + | VernacAssumption _ + | VernacCoercion _ | VernacIdentityCoercion _ + | VernacInstance _ | VernacDeclareInstances _ + | VernacDeclareMLModule _ + | VernacDeclareTacticDefinition _ + | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ + | VernacSyntacticDefinition _ + | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ + | VernacGeneralizable _ + | VernacSetOpacity _ | VernacSetStrategy _ + | VernacSetOption _ | VernacUnsetOption _ + | VernacDeclareReduction _ + | VernacExtend _ ) -> () + | Some _, _ -> Errors.error "This command does not support Locality" let interp c = - let mode = Flags.is_program_mode () in - let isprogcmd = !Flags.program_cmd in - Flags.program_cmd := false; - Obligations.set_program_mode isprogcmd; - try - interp c; Locality.check_locality (); - if not (not mode && !Flags.program_mode && not isprogcmd) then - Flags.program_mode := mode; - true - with - | UnsafeSuccess -> - Flags.program_mode := mode; - false - | reraise -> - let e = Errors.push reraise in - Flags.program_mode := mode; - raise e + let orig_program_mode = Flags.is_program_mode () in + let rec aux ?locality isprogcmd = function + | VernacProgram c when not isprogcmd -> aux ?locality true c + | VernacProgram _ -> Errors.error "Program mode specified twice" + | VernacLocal (b, c) when locality = None -> aux ~locality:b isprogcmd c + | VernacLocal _ -> Errors.error "Locality specified twice" + | c -> + check_vernac_supports_locality c locality; + Obligations.set_program_mode isprogcmd; + try + interp locality c; + if orig_program_mode || not !Flags.program_mode || isprogcmd then + Flags.program_mode := orig_program_mode; + true + with + | UnsafeSuccess -> + Flags.program_mode := orig_program_mode; + false + | reraise -> + let e = Errors.push reraise in + Flags.program_mode := orig_program_mode; + raise e + in + aux false c diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index e15edf4e9..2cc33dadc 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -40,14 +40,16 @@ let vinterp_init () = Hashtbl.clear vernac_tab (* Interpretation of a vernac command *) -let call (opn,converted_args) = +let call ?locality (opn,converted_args) = let loc = ref "Looking up command" in try let callback = vinterp_map opn in loc:= "Checking arguments"; let hunk = callback converted_args in loc:= "Executing command"; - hunk() + Locality.LocalityFixme.set locality; + hunk(); + Locality.LocalityFixme.assert_consumed() with | Drop -> raise Drop | reraise -> diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 7138c36f1..4c2b66ed8 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -15,4 +15,4 @@ val overwriting_vinterp_add : string -> (raw_generic_argument list -> unit -> unit) -> unit val vinterp_init : unit -> unit -val call : string * raw_generic_argument list -> unit +val call : ?locality:bool -> string * raw_generic_argument list -> unit |