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. --- printing/printer.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'printing/printer.mli') diff --git a/printing/printer.mli b/printing/printer.mli index 2c9a4d70e..ba849bee6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -14,6 +14,7 @@ open Pattern open Evd open Proof_type open Glob_term +open Ltac_pretype (** These are the entry points for printing terms, context, tac, ... *) -- cgit v1.2.3