aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.mli')
-rw-r--r--pretyping/classops.mli3
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