aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/btauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/btauto')
-rw-r--r--plugins/btauto/refl_btauto.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 4d2859fb0..93bd88fe4 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -221,6 +221,7 @@ module Btauto = struct
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let eq = Lazy.force eq in
+ let concl = EConstr.Unsafe.to_constr concl in
let t = decomp_term (Tacmach.New.project gl) concl in
match t with
| Term.App (c, [|typ; p; _|]) when c === eq ->
@@ -235,6 +236,7 @@ module Btauto = struct
let tac =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
+ let concl = EConstr.Unsafe.to_constr concl in
let sigma = Tacmach.New.project gl in
let eq = Lazy.force eq in
let bool = Lazy.force Bool.typ in