From 0e8fc03878b360e540069df139cbcc278837d5d2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 12 Jul 2017 17:25:33 +0200
Subject: Adding econstr printer to "include" file.

---
 dev/include | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index 31ae5da71a..0d34595f4f 100644
--- a/dev/include
+++ b/dev/include
@@ -31,6 +31,7 @@
 #install_printer  (* glob_constr *) ppglob_constr;;
 #install_printer  (* open constr *) ppopenconstr;;
 #install_printer  (* constr *) ppconstr;;
+#install_printer  (* econstr *) ppeconstr;;
 #install_printer  (* constr_substituted *) ppsconstr;; 
 #install_printer  (* constraints *)  ppconstraints;;
 #install_printer  (* univ constraints *)  ppuniverseconstraints;;
-- 
cgit v1.2.3