diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-20 18:17:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-27 19:47:52 +0100 |
| commit | 9243166490e8c939bbf6aa0316e99025b25e6398 (patch) | |
| tree | 391e1d205ee7a378774228404e5a7c00416e2d97 /vernac/vernacentries.mli | |
| parent | 6f240e9b15f2b6f6622c811933c4f5ffdf78cceb (diff) | |
[vernac] Adjust `interp` to pass polymorphic in the attributes.
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |