From 347d94a4b966d0cc4a3a04814b0c76c4b05caa11 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 Oct 2017 18:58:38 +0200
Subject: Ltac uses the new generic locatable API.

---
 API/API.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'API/API.ml')

diff --git a/API/API.ml b/API/API.ml
index 46ad36d36d..bf99d0febd 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -212,7 +212,7 @@ module Pputils = Pputils
 module Ppconstr = Ppconstr
 module Printer = Printer
 (* module Printmod *)
-(* module Prettyp *)
+module Prettyp = Prettyp
 module Ppvernac = Ppvernac
 
 (******************************************************************************)
-- 
cgit v1.2.3