diff --git a/AAC_coq.ml b/AAC_coq.ml
index b3ee180..ea1601e 100644
--- a/AAC_coq.ml
+++ b/AAC_coq.ml
@@ -27,7 +27,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
   }

 let cps_mk_letin
@@ -164,7 +164,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")
@@ -578,7 +578,7 @@ let rewrite ?(abort=false)hypinfo subst k =
 	    hypinfo.l2r
 	    Termops.all_occurrences
 	    false
-	    (rew,Rawterm.NoBindings)
+	    (rew,Glob_term.NoBindings)
 	    true
 	else
 	  Tacticals.tclIDTAC
diff --git a/Instances.v b/Instances.v
index bb309fe..c3c9732 100644
--- a/Instances.v
+++ b/Instances.v
@@ -19,7 +19,7 @@ Proof. intros x y ->. reflexivity. Qed.
 (* At the moment, all the instances are exported even if they are packaged into modules. Even using LocalInstances in fact*)

 Module Peano.
-  Require Import Arith NArith Max.
+  Require Import Arith NArith Max Min.
   Instance aac_plus_Assoc : Associative eq plus := plus_assoc.
   Instance aac_plus_Comm : Commutative eq plus :=  plus_comm.

@@ -82,7 +82,7 @@ End Lists.


 Module N.
-  Require Import NArith Nminmax.
+  Require Import NArith.
   Open Scope N_scope.
   Instance aac_Nplus_Assoc : Associative eq Nplus :=  Nplus_assoc.
   Instance aac_Nplus_Comm : Commutative eq Nplus :=  Nplus_comm.