diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |