From bf4112094feb1a705d8bdaea3fb0febc4ef3ff59 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 24 Oct 2017 14:35:25 +0200
Subject: [general] Remove Econstr dependency from `intf`

To this extent we factor out the relevant bits to a new file,
ltac_pretype.
---
 API/API.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'API/API.ml')

diff --git a/API/API.ml b/API/API.ml
index bf99d0febd..6e61063e4b 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -131,6 +131,7 @@ module Geninterp = Geninterp
 (******************************************************************************)
 (* Pretyping                                                                  *)
 (******************************************************************************)
+module Ltac_pretype = Ltac_pretype
 module Locusops = Locusops
 module Pretype_errors = Pretype_errors
 module Reductionops = Reductionops
-- 
cgit v1.2.3