aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/firstorder/unify.ml4
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index eebd974ea..a3513692c 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
let typ=pf_unsafe_type_of gl idc in
(* since we know we will get a product,
reduction is not too expensive *)
- let (nam,_,_)=destProd (whd_all env evmap typ) in
+ let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in
match nam with
Name id -> id
| Anonymous -> dummy_bvid in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 01c019744..fb237f29b 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -41,8 +41,8 @@ let unif t1 t2=
Queue.add (t1,t2) bige;
try while true do
let t1,t2=Queue.take bige in
- let nt1=head_reduce (whd_betaiotazeta Evd.empty t1)
- and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
+ let nt1=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t1))
+ and nt2=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t2)) in
match (kind_of_term nt1),(kind_of_term nt2) with
Meta i,Meta j->
if not (Int.equal i j) then