aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_classes.ml')
-rw-r--r--plugins/subtac/subtac_classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index fccb2f9332..88f88b7f25 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -28,7 +28,7 @@ module SPretyping = Subtac_pretyping.Pretyping
let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
SPretyping.understand_tcc_evars evdref env kind
- (intern_gen (kind=IsType) ~impls ( !evdref) env c)
+ (intern_gen (kind=IsType) ~impls !evdref env c)
let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c