aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r--toplevel/record.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 96221b742..73035deb0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -375,7 +375,7 @@ let structure_signature ctx =
let evm = Sigma.to_evar_map evm in
let new_tl = Util.List.map_i
(fun pos decl ->
- RelDecl.map_type (fun t -> Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t)) decl) 1 tl in
+ RelDecl.map_type (fun t -> EConstr.Unsafe.to_constr (Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t))) decl) 1 tl in
deps_to_evar evm new_tl in
deps_to_evar Evd.empty (List.rev ctx)