aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.mli')
-rw-r--r--pretyping/classops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index b41d0efac..47b41f17b 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -96,7 +96,7 @@ val lookup_pattern_path_between :
(**/**)
(* Crade *)
val install_path_printer :
- ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+ (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
(**/**)
(** {6 This is for printing purpose } *)