aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 977146b2f..c2157bb2e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2123,7 +2123,7 @@ let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ =
- interp_constr_evars_gen env evdref ~impls (OfType (EConstr.of_constr typ)) c
+ interp_constr_evars_gen env evdref ~impls (OfType typ) c
let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
interp_constr_evars_gen env evdref IsType ~impls c