From 9243166490e8c939bbf6aa0316e99025b25e6398 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 20 Nov 2017 18:17:58 +0100 Subject: [vernac] Adjust `interp` to pass polymorphic in the attributes. --- 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 67001bc24..a559912a0 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 -> - Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t + st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> 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