aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 548ca7596f..b0554540af 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -143,7 +143,7 @@ let coercion_params coe_info = coe_info.coe_param
(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
let find_class_type env sigma t =
- let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in
+ let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
match kind_of_term t' with
| Var id -> CL_SECVAR id, args
| Const sp -> CL_CONST sp, args