aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/find_subterm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/find_subterm.ml')
-rw-r--r--pretyping/find_subterm.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index d09686f6e..3fc569fc4 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -64,8 +64,8 @@ let proceed_with_occurrences f occs x =
let map_named_declaration_with_hyploc f hyploc acc decl =
let open Context.Named.Declaration in
let f acc typ =
- let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc (EConstr.of_constr typ) in
- acc, EConstr.Unsafe.to_constr typ
+ let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc typ in
+ acc, typ
in
match decl,hyploc with
| LocalAssum (id,_), InHypValueOnly ->