From 6f240e9b15f2b6f6622c811933c4f5ffdf78cceb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 20 Nov 2017 16:28:02 +0100
Subject: [vernac] Add polymorphic to the type of vernac interpration options.

---
 vernac/vernacinterp.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/vernacinterp.mli')

diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index fc528579f..ab3d4bfc5 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -13,6 +13,7 @@ type deprecation = bool
 type atts = {
   loc : Loc.t option;
   locality : bool option;
+  polymorphic : bool;
 }
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
-- 
cgit v1.2.3