From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 22:16:08 +0100 Subject: Proofview.Goal primitive now return EConstrs. --- plugins/btauto/refl_btauto.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'plugins/btauto/refl_btauto.ml') 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 -- cgit v1.2.3