diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/pvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/pvernac.mli | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 0e46df2320..994fad85f0 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -52,7 +52,7 @@ module Vernac_ = let () = let open Extend in - let act_vernac v loc = Some (loc, v) in + let act_vernac v loc = Some CAst.(make ~loc v) in let act_eoi _ loc = None in let rule = [ Rule (Next (Stop, Atoken Tok.EOI), act_eoi); diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index fa251281dc..4bf7c9f7bd 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -26,7 +26,7 @@ module Vernac_ : val rec_definition : (fixpoint_expr * decl_notation list) Entry.t val noedit_mode : vernac_expr Entry.t val command_entry : vernac_expr Entry.t - val main_entry : (Loc.t * vernac_control) option Entry.t + val main_entry : vernac_control CAst.t option Entry.t val red_expr : raw_red_expr Entry.t val hint_info : Hints.hint_info_expr Entry.t end @@ -40,7 +40,7 @@ module Unsafe : sig end (** The main entry: reads an optional vernac command *) -val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t +val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t (** Grammar entry for tactics: proof mode(s). By default Coq's grammar has an empty entry (non-terminal) for diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7611355100..a5ef41c4db 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2167,7 +2167,7 @@ let vernac_load interp fname = else None in - interp (snd (parse_sentence proof_mode input)); + interp (parse_sentence proof_mode input).CAst.v; done with End_of_input -> () end; |