diff options
| -rw-r--r-- | vernac/attributes.ml | 5 | ||||
| -rw-r--r-- | vernac/attributes.mli | 3 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 13 |
3 files changed, 9 insertions, 12 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 2f1f6e04e3..2bef6ff320 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -14,7 +14,6 @@ let mk_deprecation ?(since=None) ?(note=None) () = { since ; note } type t = { - loc : Loc.t option; locality : bool option; polymorphic : bool; template : bool option; @@ -22,5 +21,5 @@ type t = { deprecated : deprecation option; } -let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () = - { loc ; locality ; polymorphic ; program ; deprecated; template } +let mk_atts ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () = + { locality ; polymorphic ; program ; deprecated; template } diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 571f0ddd7d..b8dcde5655 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -13,7 +13,6 @@ type deprecation = { since : string option ; note : string option } val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation type t = { - loc : Loc.t option; locality : bool option; polymorphic : bool; template : bool option; @@ -21,6 +20,6 @@ type t = { deprecated : deprecation option; } -val mk_atts : ?loc: Loc.t option -> ?locality: bool option -> +val mk_atts : ?locality: bool option -> ?polymorphic: bool -> ?template:bool option -> ?program: bool -> ?deprecated: deprecation option -> unit -> t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 391e8f7990..57585f11c7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -740,14 +740,14 @@ let vernac_combined_scheme lid l = let vernac_universe ~atts l = if atts.polymorphic && not (Lib.sections_are_opened ()) then - user_err ?loc:atts.loc ~hdr:"vernac_universe" + user_err ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); Declare.do_universe atts.polymorphic l let vernac_constraint ~atts l = if atts.polymorphic && not (Lib.sections_are_opened ()) then - user_err ?loc:atts.loc ~hdr:"vernac_constraint" + user_err ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); Declare.do_constraint atts.polymorphic l @@ -1721,7 +1721,7 @@ let query_command_selector ?loc = function (str "Query commands only support the single numbered goal selector.") let vernac_check_may_eval ~atts redexp glopt rc = - let glopt = query_command_selector ?loc:atts.loc glopt in + let glopt = query_command_selector glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma, c = interp_open_constr env sigma rc in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in @@ -1815,7 +1815,6 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~atts env sigma = - let loc = atts.loc in function | PrintTables -> print_tables () | PrintFullContext-> print_full_context_typ env sigma @@ -1863,7 +1862,7 @@ let vernac_print ~atts env sigma = | PrintVisibility s -> Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> - print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt + print_about_hyp_globs ref_or_by_not udecl glnumopt | PrintImplicit qid -> dump_global qid; print_impargs qid @@ -1929,7 +1928,7 @@ let _ = optwrite = (:=) search_output_name_only } let vernac_search ~atts s gopt r = - let gopt = query_command_selector ?loc:atts.loc gopt in + let gopt = query_command_selector gopt in let r = interp_search_restriction r in let env,gopt = match gopt with | None -> @@ -2255,7 +2254,7 @@ let interp ?proof ~atts ~st c = let using = Option.append using (Proof_using.get_default_proof_using ()) in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in let usings = if Option.is_empty using then "using:no" else "using:yes" in - Aux_file.record_in_aux_at ?loc:atts.loc "VernacProof" (tacs^" "^usings); + Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings); Option.iter vernac_set_end_tac tac; Option.iter vernac_set_used_variables using | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] |