aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/derive
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/derive')
-rw-r--r--plugins/derive/derive.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e39d17b52..f23f4ce7d 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -37,6 +37,7 @@ let start_deriving f suchthat lemma =
let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
let evdref = ref sigma in
let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
+ let suchthat = EConstr.Unsafe.to_constr suchthat in
TCons ( env' , !evdref , suchthat , (fun sigma _ ->
TNil sigma))))))
in