From beb5875cca7648ba9963c99a68ea22494ab6329b Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 5 Nov 2016 16:28:23 +0100
Subject: FIX: dev/include

---
 dev/include | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index d82fb74f22..9068688f19 100644
--- a/dev/include
+++ b/dev/include
@@ -47,7 +47,6 @@
 #install_printer  (* univ full subst *) ppuniverse_level_subst;;
 #install_printer  (* univ opt subst *) ppuniverse_opt_subst;;
 #install_printer  (* evar univ ctx *) ppevar_universe_context;;
-#install_printer  (* constraints_map *) ppconstraints_map;;
 #install_printer  (* inductive *) ppind;;
 #install_printer  (* 'a scheme_kind *) ppscheme;;
 #install_printer  (* type_judgement *) pptype;;
-- 
cgit v1.2.3