From 6c28c8f38c6f47cc772d42e5cc54398785d63bc0 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 23 Nov 1999 17:39:25 +0000
Subject: modules Indrec, Tacentries, Hiddentac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@131 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 5f8cfefc01..823917ea5f 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 (*i*)
+open Pp
 open Names
 open Generic
 (*i*)
@@ -39,6 +40,8 @@ type sorts =
 val mk_Set  : sorts
 val mk_Prop : sorts
 
+val print_sort : sorts -> std_ppcmds
+
 (*s The type [constr] of the terms of CCI
   is obtained by instanciating the generic terms (type [term], 
   see \refsec{generic_terms}) on the above operators, themselves instanciated
-- 
cgit v1.2.3