aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/indschemes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/indschemes.ml')
-rw-r--r--toplevel/indschemes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index e0b861e0a..48521a8e5 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -161,7 +161,7 @@ let try_declare_scheme what f internal names kn =
let msg = match fst e with
| ParameterWithoutEquality cst ->
alarm what internal
- (str "Boolean equality not found for parameter " ++ pr_con cst ++
+ (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++
str".")
| InductiveWithProduct ->
alarm what internal