aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/redops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/redops.ml')
-rw-r--r--pretyping/redops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index db5879174..7d65925e5 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -20,12 +20,12 @@ let make_red_flag l =
| FZeta :: lf -> add_flag { red with rZeta = true } lf
| FConst l :: lf ->
if red.rDelta then
- Errors.error
+ CErrors.error
"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
- Errors.error
+ CErrors.error
"Cannot set both constants to unfold and constants not to unfold";
add_flag
{ red with rConst = union_consts red.rConst l; rDelta = true }