diff options
Diffstat (limited to 'pretyping/classops.mli')
-rw-r--r-- | pretyping/classops.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 890aa005c..6184ed7a1 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -82,7 +82,8 @@ val lookup_path_to_sort_from : env -> evar_map -> types -> val lookup_pattern_path_between : inductive * inductive -> (constructor * int) list -(*i Crade *) +(**/**) +(* Crade *) open Pp val install_path_printer : ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit |