aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/perror.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness/perror.ml')
-rw-r--r--contrib/correctness/perror.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 1eb44d5bc..452e1b581 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -66,7 +66,7 @@ let is_constant_type s = function
TypePure c ->
let id = id_of_string s in
let c' = Declare.global_reference id in
- Reduction.is_conv (Global.env()) Evd.empty c c'
+ Reductionops.is_conv (Global.env()) Evd.empty c c'
| _ -> false
let check_for_index_type loc v =