From 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 14 Feb 2018 06:57:40 +0100 Subject: [located] More work towards using CAst.t We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes. --- vernac/vernacentries.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/vernacentries.mli') diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 13ecaf37b..f6199e820 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -20,7 +20,7 @@ val vernac_require : val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - st:Vernacstate.t -> Vernacexpr.vernac_control Loc.located -> Vernacstate.t + st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name -- cgit v1.2.3