diff --git a/Instances.v b/Instances.v
index 1a2e08f..ef9a2e6 100644
--- a/Instances.v
+++ b/Instances.v
@@ -13,8 +13,8 @@
 Require Export  AAC.

 Module Peano.
-  Require Import Arith NArith Max.
-  Program Instance aac_plus : @Op_AC nat eq plus 0 := @Build_Op_AC nat (@eq nat) plus 0  _ plus_0_l plus_assoc plus_comm.
+  Require Import Arith Max.
+  Instance aac_plus : @Op_AC nat eq plus 0 := @Build_Op_AC nat (@eq nat) plus 0 _ plus_0_l plus_assoc plus_comm.


   Program Instance aac_mult : Op_AC eq mult 1 := Build_Op_AC _ _ _ mult_assoc mult_comm.
diff --git a/coq.ml b/coq.ml
index 731204c..9994fe0 100644
--- a/coq.ml
+++ b/coq.ml
@@ -29,7 +29,7 @@ let init_constant dir s = find_constant contrib_name dir s
    in the goal *)
 let nowhere =
   { Tacexpr.onhyps = Some [];
-    Tacexpr.concl_occs = Rawterm.no_occurrences_expr
+    Tacexpr.concl_occs = Glob_term.no_occurrences_expr
   }


@@ -97,7 +97,7 @@ end

 module Pos = struct

-    let path = ["Coq" ; "NArith"; "BinPos"]
+    let path = ["Coq" ; "PArith"; "BinPos"]
     let typ = lazy (init_constant path "positive")
     let xI =      lazy (init_constant path "xI")
     let xO =      lazy (init_constant path "xO")
@@ -144,7 +144,7 @@ end

 (** Lists from the standard library*)
 module List = struct
-  let path = ["Coq"; "Lists"; "List"]
+  let path = ["Coq"; "Init"; "Datatypes"]
   let typ = lazy (init_constant path "list")
   let nil = lazy (init_constant path "nil")
   let cons = lazy (init_constant path "cons")
diff --git a/theory.ml b/theory.ml
index 45a76f1..08a2dcb 100644
--- a/theory.ml
+++ b/theory.ml
@@ -666,13 +666,11 @@ module Trans = struct
     let env_sum, env_sum_letin = Coq.mk_letin "env_sum_name" (s.env_sum) in
     let s = {env_sym = env_sym; env_prd = env_prd; env_sum = env_sum} in
     let rb , tac = mk_reif_builders (fst eqt) (s.env_sym) in
-    let evar_map = Tacmach.project goal in
     let tac = Tacticals.tclTHENLIST (
-      [		       Refiner.tclEVARS evar_map;
-		       env_prd_letin ;
-		       env_sum_letin ;
-		       env_sym_letin ;
-		       tac
+      [ env_prd_letin ;
+        env_sum_letin ;
+        env_sym_letin ;
+        tac
       ]) in
       s, (sm, rb), tac