diff options
Diffstat (limited to 'contrib/funind/indfun_common.mli')
| -rw-r--r-- | contrib/funind/indfun_common.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli index ab5195b07..8385eef20 100644 --- a/contrib/funind/indfun_common.mli +++ b/contrib/funind/indfun_common.mli @@ -2,6 +2,9 @@ open Names open Pp val mk_rel_id : identifier -> identifier +val mk_correct_id : identifier -> identifier +val mk_complete_id : identifier -> identifier +val mk_equation_id : identifier -> identifier val msgnl : std_ppcmds -> unit |