From 1655407ac0525efa0fcd98ab85e3fd80a9f6cf64 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 24 Nov 2018 20:22:23 +0100
Subject: [gramlib] Minor cleanups:

- remove duplicate type definitions `gram_assoc`, `gram_position`,
- make global `warning_verbose` variable into a parameter.
---
 plugins/ltac/tacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index ac2d88dec2..2aee809eb6 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -119,7 +119,7 @@ let get_tactic_entry n =
   else if Int.equal n 5 then
     Pltac.binder_tactic, None
   else if 1<=n && n<5 then
-    Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
+    Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n))
   else
     user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
 
-- 
cgit v1.2.3