aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/redops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/redops.ml')
-rw-r--r--pretyping/redops.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index 7d65925e5..8e190f40b 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -20,13 +20,13 @@ let make_red_flag l =
| FZeta :: lf -> add_flag { red with rZeta = true } lf
| FConst l :: lf ->
if red.rDelta then
- CErrors.error
- "Cannot set both constants to unfold and constants not to unfold";
+ CErrors.user_err Pp.(str
+ "Cannot set both constants to unfold and constants not to unfold");
add_flag { red with rConst = union_consts red.rConst l } lf
| FDeltaBut l :: lf ->
if red.rConst <> [] && not red.rDelta then
- CErrors.error
- "Cannot set both constants to unfold and constants not to unfold";
+ CErrors.user_err Pp.(str
+ "Cannot set both constants to unfold and constants not to unfold");
add_flag
{ red with rConst = union_consts red.rConst l; rDelta = true }
lf