diff options
Diffstat (limited to 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 2 |
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 |