diff options
| author | Enrico Tassi | 2021-02-10 13:07:47 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-02-11 18:11:01 +0100 |
| commit | 13b22836272ebf66b3e07bab9a5d1ec253194c95 (patch) | |
| tree | dca0b6e91504a45e554ab406286d195687f206c3 /vernac/vernacextend.ml | |
| parent | 16765871394a81975047b37f15a902fcc112dc40 (diff) | |
[vernac] pass the loc of the whole command to the interp function
Diffstat (limited to 'vernac/vernacextend.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 *) |