diff options
Diffstat (limited to 'checker/indtypes.mli')
| -rw-r--r-- | checker/indtypes.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/indtypes.mli b/checker/indtypes.mli index 7eaaf65f2..b0554989e 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -12,8 +12,8 @@ open Cic open Environ (*i*) -val prkn : kernel_name -> Pp.std_ppcmds -val prcon : constant -> Pp.std_ppcmds +val prkn : kernel_name -> Pp.t +val prcon : constant -> Pp.t (*s The different kinds of errors that may result of a malformed inductive definition. *) |