From a95210435f336d89f44052170a7c65563e6e35f2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 24 Sep 2014 22:19:46 +0200
Subject: Index keys instead of simply global references.

---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 4afa9d4fc9..1d09ce105e 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -109,6 +109,7 @@ Goptions
 Decls
 Heads
 Assumptions
+Keys
 Locusops
 Miscops
 Universes
-- 
cgit v1.2.3