diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 3 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 8 |
5 files changed, 12 insertions, 11 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 481bc3071b..664c6b2f36 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2064,7 +2064,7 @@ let vernac_check_guard ~pstate = (* We interpret vernacular commands to a DSL that specifies their allowed actions on proof states *) -let translate_vernac ~atts v = let open Vernacextend in match v with +let translate_vernac ?loc ~atts v = let open Vernacextend in match v with | VernacAbortAll | VernacRestart | VernacUndo _ @@ -2389,4 +2389,4 @@ let translate_vernac ~atts v = let open Vernacextend in match v with (* Extensions *) | VernacExtend (opn,args) -> - Vernacextend.type_vernac ~atts opn args + Vernacextend.type_vernac ?loc ~atts opn args diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 2ac8458ad5..b30bbc3ce7 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -10,7 +10,8 @@ (** Vernac Translation into the Vernac DSL *) val translate_vernac - : atts:Attributes.vernac_flags + : ?loc:Loc.t + -> atts:Attributes.vernac_flags -> Vernacexpr.vernac_expr -> Vernacextend.typed_vernac diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index f320b65954..df82382041 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -64,7 +64,7 @@ type typed_vernac = | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) -type vernac_command = atts:Attributes.vernac_flags -> typed_vernac +type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> typed_vernac type plugin_args = Genarg.raw_generic_argument list @@ -94,7 +94,7 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) -let type_vernac opn converted_args ~atts = +let type_vernac opn converted_args ?loc ~atts = let depr, callback = vinterp_map opn in let () = if depr then let rules = Egramml.get_extend_vernac_rule opn in @@ -106,7 +106,7 @@ let type_vernac opn converted_args ~atts = warn_deprecated_command pr; in let hunk = callback converted_args in - hunk ~atts + hunk ?loc ~atts (** VERNAC EXTEND registering *) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 070c737882..27f6930dec 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -82,7 +82,7 @@ type typed_vernac = | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) -type vernac_command = atts:Attributes.vernac_flags -> typed_vernac +type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> typed_vernac type plugin_args = Genarg.raw_generic_argument list diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index e42775b76c..4098401bf0 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -151,7 +151,7 @@ let interp_control_flag ~time_header (f : control_flag) ~st * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) -let rec interp_expr ~atts ~st c = +let rec interp_expr ?loc ~atts ~st c = let stack = st.Vernacstate.lemmas in let program = st.Vernacstate.program in vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); @@ -174,7 +174,7 @@ let rec interp_expr ~atts ~st c = Attributes.unsupported_attributes atts; vernac_load ~verbosely fname | v -> - let fv = Vernacentries.translate_vernac ~atts v in + let fv = Vernacentries.translate_vernac ?loc ~atts v in interp_typed_vernac ~pm:program ~stack fv and vernac_load ~verbosely fname = @@ -206,13 +206,13 @@ and vernac_load ~verbosely fname = CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); stack, pm -and interp_control ~st ({ CAst.v = cmd } as vernac) = +and interp_control ~st ({ CAst.v = cmd; loc } as vernac) = let time_header = mk_time_header vernac in List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) cmd.control (fun ~st -> let before_univs = Global.universes () in - let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in + let pstack, pm = interp_expr ?loc ~atts:cmd.attrs ~st cmd.expr in let after_univs = Global.universes () in if before_univs == after_univs then pstack, pm else |