1 files changed, 29 insertions, 30 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6e8b2eb0..a09abfa1 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,5 +1,3 @@
-open Proofview.Notations
-
 let contrib_name = "btauto"
 
 let init_constant dir s =
@@ -8,18 +6,18 @@ 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 : Constr.t) =
+  Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c)))
 
-let lapp c v  = Term.mkApp (Lazy.force c, v)
+let lapp c v  = Constr.mkApp (Lazy.force c, v)
 
-let (===) = Term.eq_constr
+let (===) = Constr.equal
 
 module CoqList = struct
   let path = ["Init"; "Datatypes"]
@@ -55,17 +53,11 @@ end
 
 module Env = struct
 
-  module ConstrHashed = struct
-    type t = Term.constr
-    let equal = Term.eq_constr
-    let hash = Term.hash_constr
-  end
-
-  module ConstrHashtbl = Hashtbl.Make (ConstrHashed)
+  module ConstrHashtbl = Hashtbl.Make (Constr)
 
   type t = (int ConstrHashtbl.t * int ref)
 
-  let add (tbl, off) (t : Term.constr) =
+  let add (tbl, off) (t : Constr.t) =
     try ConstrHashtbl.find tbl t 
     with
     | Not_found -> 
@@ -105,7 +97,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 : Constr.t) : t =
     let trueb = Lazy.force trueb in
     let falseb = Lazy.force falseb in
     let andb = Lazy.force andb in
@@ -113,7 +105,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))
@@ -172,16 +164,18 @@ module Btauto = struct
   | Bool.Xorb (b1, b2) -> lapp f_xor [|convert b1; convert b2|]
   | Bool.Ifb (b1, b2, b3) -> lapp f_ifb [|convert b1; convert b2; convert b3|]
 
-  let convert_env env : Term.constr = 
+  let convert_env env : Constr.t = 
     CoqList.of_list (Lazy.force Bool.typ) env
 
   let reify env t = lapp eval [|convert_env env; convert t|]
 
   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|])
@@ -206,7 +200,8 @@ module Btauto = struct
         let assign = List.combine env var in
         let map_msg (key, v) =
           let b = if v then str "true" else str "false" in
-          let term = Printer.pr_constr key in
+          let sigma, env = Pfedit.get_current_context () in
+          let term = Printer.pr_constr_env env sigma key in
           term ++ spc () ++ str ":=" ++ spc () ++ b
         in
         let assign = List.map map_msg assign in
@@ -217,10 +212,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 +225,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 = Constr.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