3 files changed, 24 insertions, 19 deletions

diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4
index f1e0081987..23b91507c9 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "btauto_plugin"
 
 TACTIC EXTEND btauto
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6e8b2eb0fb..00e80d041f 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,4 +1,4 @@
-open Proofview.Notations
+open API
 
 let contrib_name = "btauto"
 
@@ -8,14 +8,14 @@ let init_constant dir s =
   in
   find_constant contrib_name dir s
 
-let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s)
+let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s)
 
 let get_inductive dir s =
   let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
   Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ()))
 
-let decomp_term (c : Term.constr) =
-  Term.kind_of_term (Term.strip_outer_cast c)
+let decomp_term sigma (c : Term.constr) =
+  Term.kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c)))
 
 let lapp c v  = Term.mkApp (Lazy.force c, v)
 
@@ -105,7 +105,7 @@ module Bool = struct
   | Negb of t
   | Ifb of t * t * t
 
-  let quote (env : Env.t) (c : Term.constr) : t =
+  let quote (env : Env.t) sigma (c : Term.constr) : t =
     let trueb = Lazy.force trueb in
     let falseb = Lazy.force falseb in
     let andb = Lazy.force andb in
@@ -113,7 +113,7 @@ module Bool = struct
     let xorb = Lazy.force xorb in
     let negb = Lazy.force negb in
 
-    let rec aux c = match decomp_term c with
+    let rec aux c = match decomp_term sigma c with
     | Term.App (head, args) ->
       if head === andb && Array.length args = 2 then
         Andb (aux args.(0), aux args.(1))
@@ -179,9 +179,11 @@ module Btauto = struct
 
   let print_counterexample p env gl =
     let var = lapp witness [|p|] in
+    let var = EConstr.of_constr var in
     (* Compute an assignment that dissatisfies the goal *)
     let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
-    let rec to_list l = match decomp_term l with
+    let var = EConstr.Unsafe.to_constr var in
+    let rec to_list l = match decomp_term (Tacmach.project gl) l with
     | Term.App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
     | Term.App (c, [|_; h; t|])
@@ -217,10 +219,11 @@ module Btauto = struct
     Tacticals.tclFAIL 0 msg gl
 
   let try_unification env =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.nf_enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let eq = Lazy.force eq in
-      let t = decomp_term concl 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 ->
       (* should be an equality [@eq poly ?p (Cst false)] *)
@@ -229,33 +232,36 @@ module Btauto = struct
       | _ ->
           let msg = str "Btauto: Internal error" in
           Tacticals.New.tclFAIL 0 msg
-    end }
+    end
 
   let tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.nf_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
-      let t = decomp_term concl in
+      let t = decomp_term sigma concl in
       match t with
       | Term.App (c, [|typ; tl; tr|])
           when typ === bool && c === eq ->
           let env = Env.empty () in
-          let fl = Bool.quote env tl in
-          let fr = Bool.quote env tr in
+          let fl = Bool.quote env sigma tl in
+          let fr = Bool.quote env sigma tr in
           let env = Env.to_list env in
           let fl = reify env fl in
           let fr = reify env fr in
           let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
+          let changed_gl = EConstr.of_constr changed_gl in
           Tacticals.New.tclTHENLIST [
             Tactics.change_concl changed_gl;
-            Tactics.apply (Lazy.force soundness);
+            Tactics.apply (EConstr.of_constr (Lazy.force soundness));
             Tactics.normalise_vm_in_concl;
             try_unification env
           ]
       | _ ->
           let msg = str "Cannot recognize a boolean equality" in
           Tacticals.New.tclFAIL 0 msg
-    end }
+    end
 
 end
diff --git a/plugins/btauto/vo.itarget b/plugins/btauto/vo.itarget
deleted file mode 100644
index 1f72d3ef22..0000000000
--- a/plugins/btauto/vo.itarget
+++ /dev/null
@@ -1,3 +0,0 @@
-Algebra.vo
-Reflect.vo
-Btauto.vo