summaryrefslogtreecommitdiff
path: root/contrib/funind/indfun.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind/indfun.ml')
-rw-r--r--contrib/funind/indfun.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 82bb2869..6e2af224 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -266,7 +266,7 @@ let derive_inversion fix_names =
)
with e ->
msg_warning
- (str "Cannot built inversion information" ++
+ (str "Cannot build functional inversion principle" ++
if do_observe () then Cerrors.explain_exn e else mt ())
with _ -> ()