From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 23:40:35 +0100 Subject: [location] Remove Loc.ghost. Now it is a private field, locations are optional. --- 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 fb2899515..f75f7656d 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -18,7 +18,7 @@ val vernac_require : val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Loc.t * Vernacexpr.vernac_expr -> unit + Vernacexpr.vernac_expr Loc.located -> unit (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name -- cgit v1.2.3