diff --git a/README.md b/README.md
index 27970b7..a66978c 100644
--- a/README.md
+++ b/README.md
@@ -108,10 +108,11 @@ Namely, it contains instances for:
 
 - Peano naturals	(`Import Instances.Peano.`)
 - Z binary numbers	(`Import Instances.Z.`)
+- Lists    		(`Import Instances.Lists.`)
 - N binary numbers	(`Import Instances.N.`)
 - P binary numbers	(`Import Instances.P.`)
 - Rational numbers	(`Import Instances.Q.`)
-- Prop			(`Import Instances.Prop_ops.`)
+- Prop    		(`Import Instances.Prop_ops.`)
 - Booleans		(`Import Instances.Bool.`)
 - Relations		(`Import Instances.Relations.`)
 - all of the above	(`Import Instances.All.`)
diff --git a/meta.yml b/meta.yml
index 604e9bf..d66bf33 100644
--- a/meta.yml
+++ b/meta.yml
@@ -109,10 +109,11 @@ documentation: |
   
   - Peano naturals	(`Import Instances.Peano.`)
   - Z binary numbers	(`Import Instances.Z.`)
+  - Lists    		(`Import Instances.Lists.`)
   - N binary numbers	(`Import Instances.N.`)
   - P binary numbers	(`Import Instances.P.`)
   - Rational numbers	(`Import Instances.Q.`)
-  - Prop			(`Import Instances.Prop_ops.`)
+  - Prop    		(`Import Instances.Prop_ops.`)
   - Booleans		(`Import Instances.Bool.`)
   - Relations		(`Import Instances.Relations.`)
   - all of the above	(`Import Instances.All.`)
diff --git a/src/aac_rewrite.ml b/src/aac_rewrite.ml
index a7a0edf..f630722 100644
--- a/src/aac_rewrite.ml
+++ b/src/aac_rewrite.ml
@@ -232,7 +232,8 @@ let aac_reflexivity : unit Proofview.tactic =
         mkApp (Coq.get_efresh (Theory.Stubs.lift_reflexivity),
 	       [| x; r; lift.e.Coq.Equivalence.eq; lift.lift; reflexive |])
       in
-      Unsafe.tclEVARS sigma 
+      Unsafe.tclEVARS sigma
+      <*> Coq.tclRETYPE lift_reflexivity
       <*> Tactics.apply lift_reflexivity
       <*> (let concl = Goal.concl goal in
            tclEVARMAP >>= fun sigma ->
diff --git a/theories/AAC.v b/theories/AAC.v
index 62ca07a..40579e4 100644
--- a/theories/AAC.v
+++ b/theories/AAC.v
@@ -6,7 +6,7 @@
 (*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
 (***************************************************************************)
 
-(** * Theory file for the aac_rewrite tactic
+(** * Theory for AAC Tactics
 
    We define several base classes to package associative and possibly
    commutative/idempotent operators, and define a data-type for reified (or
@@ -26,21 +26,19 @@
    where one occurrence of [+] operates on nat while the other one
    operates on positive. *)
 
-Require Import Arith NArith.
-Require Import List.
-Require Import FMapPositive FMapFacts.
-Require Import RelationClasses Equality.
-Require Export Morphisms.
-
-From AAC_tactics
-Require Import Utils Constants.
+From Coq Require Import Arith NArith List.
+From Coq Require Import FMapPositive FMapFacts RelationClasses Equality.
+From Coq Require Export Morphisms.
+From AAC_tactics Require Import Utils Constants.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 
 Local Open Scope signature_scope.
 
-(** * Environments for the reification process: we use positive maps to index elements *)
+(** ** Environments for the reification process
+
+  We use positive maps to index elements. *)
 
 Section sigma.
   Definition sigma := PositiveMap.t.
@@ -57,8 +55,7 @@ Section sigma.
   Register sigma_empty as aac_tactics.sigma.empty.
 End sigma.
 
-
-(** * Classes for properties of operators *)
+(** ** Classes for properties of operators *)
 
 Class Associative (X:Type) (R:relation X) (dot: X -> X -> X) :=
   law_assoc : forall x y z, R (dot x (dot y z)) (dot (dot x y) z).
@@ -75,7 +72,6 @@ Register Commutative as aac_tactics.classes.Commutative.
 Register Idempotent as aac_tactics.classes.Idempotent.
 Register Unit as aac_tactics.classes.Unit.
 
-
 (** Class used to find the equivalence relation on which operations
    are A or AC, starting from the relation appearing in the goal *)
 
@@ -88,9 +84,8 @@ Register aac_lift_equivalence as aac_tactics.internal.aac_lift_equivalence.
 
 (** simple instances, when we have a subrelation, or an equivalence *)
 
-#[global]
-Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E}
-  {HR: @Transitive X R} {HER: subrelation E R}: AAC_lift  R E | 3.
+#[export] Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E}
+ {HR: @Transitive X R} {HER: subrelation E R} : AAC_lift R E | 3.
 Proof.
   constructor; trivial.
   intros ? ? H ? ? H'. split; intro G.
@@ -98,14 +93,12 @@ Proof.
    rewrite H, G. apply HER. symmetry. apply H'.
 Qed.
 
-#[global]
-Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E}
-  {HR: Proper (E==>E==>iff) R}: AAC_lift  R E | 4 := {}.
-
+#[export] Instance aac_lift_proper {X} {R : relation X} {E}
+ {HE: Equivalence E} {HR: Proper (E==>E==>iff) R} : AAC_lift  R E | 4 := {}.
 
+(** ** Utilities for the evaluation function *)
 
 Module Internal.
-(** * Utilities for the evaluation function *)
 
 Section copy.
 
@@ -132,7 +125,7 @@ Section copy.
   Lemma copy_Psucc : forall n x, R (copy (Pos.succ n) x) (plus x (copy n x)).
   Proof. intros; unfold copy; rewrite Prect_succ. reflexivity. Qed.
 
-  Global Instance copy_compat n: Proper (R ==> R) (copy n).
+  #[export] Instance copy_compat n: Proper (R ==> R) (copy n).
   Proof.
     unfold copy.
     induction n using Pind; intros x y H.
@@ -142,9 +135,9 @@ Section copy.
 
 End copy.
 
-(** * Packaging structures *)
+(** ** Packaging structures *)
 
-(** ** free symbols  *)
+(** *** Free symbols  *)
 
 Module Sym.
   Section t.
@@ -189,7 +182,7 @@ Module Sym.
 
 End Sym.
   
-(** ** binary operations *)
+(** *** Binary operations *)
 
 Module Bin.
   Section t.
@@ -211,7 +204,7 @@ Module Bin.
 End Bin.
 
 
-(** * Reification, normalisation, and decision  *)
+(** ** Reification, normalisation, and decision  *)
 
 Section s.
   Context {X} {R: relation X} {E: @Equivalence X R}.
@@ -247,8 +240,9 @@ Section s.
   #[local]
   Hint Resolve e_bin e_unit: typeclass_instances.
 
-  (** ** Almost normalised syntax
-     a term in [T] is in normal form if:
+  (** *** Almost normalised syntax
+
+     A term in [T] is in normal form if:
      - sums do not contain sums
      - products do not contain products
      - there are no unary sums or products
@@ -303,7 +297,7 @@ Section s.
  
 
 
-  (** ** Evaluation from syntax to the abstract domain *)
+  (** *** Evaluation from syntax to the abstract domain *)
 
   Fixpoint eval u: X :=
     match u with
@@ -373,7 +367,7 @@ Section s.
     match Bin.idem (e_bin i) with Some _ => true | None => false end.
 
 
-  (** ** Normalisation *)
+  (** *** Normalisation *)
 
   #[universes(template)]
   Inductive discr {A} : Type :=
@@ -519,7 +513,7 @@ Section s.
       | vcons _ u l => vcons (norm u) (vnorm l)
     end.
 
-  (** ** Correctness *)
+  (** *** Correctness *)
 
   Lemma is_unit_of_Unit  : forall i j : idx,
    is_unit_of i j = true -> Unit R (Bin.value (e_bin i)) (eval (unit j)).
@@ -554,17 +548,16 @@ Section s.
   Proof.
     destruct ((e_bin i)); auto.
   Qed.
-  #[local]
-  Hint Resolve Binvalue_Proper Binvalue_Associative Binvalue_Commutative : core.
+  #[local] Hint Resolve Binvalue_Proper Binvalue_Associative Binvalue_Commutative : core.
 
   (** auxiliary lemmas about sums  *)
 
-  #[local]
-  Hint Resolve is_unit_of_Unit : core.
+  #[local] Hint Resolve is_unit_of_Unit : core.
   Section sum_correctness.
     Variable i : idx.
     Variable is_unit : idx -> bool.
-    Hypothesis is_unit_sum_Unit : forall j, is_unit j = true->  @Unit X R (Bin.value (e_bin i)) (eval (unit j)).
+    Hypothesis is_unit_sum_Unit : forall j, is_unit j = true ->
+      @Unit X R (Bin.value (e_bin i)) (eval (unit j)).
 
     Inductive is_sum_spec_ind : T ->  @discr (mset T) -> Prop :=
     | is_sum_spec_op : forall j l, j = i -> is_sum_spec_ind (sum j l) (Is_op l)
@@ -974,8 +967,7 @@ Local Ltac internal_normalize :=
   compute [Internal.eval Utils.fold_map Internal.copy Prect]; simpl.
 
 
-(** * Lemmas for performing transitivity steps
-   given an instance of AAC_lift *)
+(** ** Lemmas for performing transitivity steps given an AAC_lift instance *)
 
 Section t.
   Context `{AAC_lift}.
diff --git a/theories/Caveats.v b/theories/Caveats.v
index 6cd43f1..c91b824 100644
--- a/theories/Caveats.v
+++ b/theories/Caveats.v
@@ -6,21 +6,16 @@
 (*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
 (***************************************************************************)
 
-(** * Currently known caveats and limitations of the [aac_tactics] library.
-
-   Depending on your installation, either uncomment the following two
-   lines, or add them to your .coqrc files, replacing "."
-   with the path to the [aac_tactics] library
-*)
-
-Require NArith PeanoNat.
+(** * Currently known caveats and limitations of AAC Tactics *)
 
+From Coq Require NArith PeanoNat.
 From AAC_tactics Require Import AAC.
 From AAC_tactics Require Instances.
 
 (** ** Limitations *)
 
-(** *** 1. Dependent parameters
+(** *** Dependent parameters
+
    The type of the rewriting hypothesis must be of the form
 
    [forall (x_1: T_1) ... (x_n: T_n), R l r],
@@ -70,13 +65,14 @@ Section parameters.
 End parameters.
 
 
-(** *** 2. Exogeneous morphisms
+(** *** Exogeneous morphisms
 
    We do not handle `exogeneous' morphisms: morphisms that move from
    type [T] to some other type [T']. *)
 
 Section morphism.
   Import NArith PeanoNat.
+  Import Instances.N Instances.Peano.
   Open Scope nat_scope.
 
   (** Typically, although [N_of_nat] is a proper morphism from
@@ -115,7 +111,7 @@ Section morphism.
 End morphism.
 
 
-(** *** 3. Treatment of variance with inequations.
+(** *** Treatment of variance with inequations
 
    We do not take variance into account when we compute the set of
    solutions to a matching problem modulo AC. As a consequence,
@@ -145,11 +141,10 @@ Section ineq.
 
 End ineq. 
 
-
-
 (** ** Caveats  *)
 
-(** *** 1. Special treatment for units.
+(** *** Special treatment for units
+
    [S O] is considered as a unit for multiplication whenever a [Peano.mult]
    appears in the goal. The downside is that [S x] does not match [1],
    and [1] does not match [S(0+0)] whenever [Peano.mult] appears in
@@ -192,11 +187,12 @@ End Peano.
 
 
 
-(** *** 2. Existential variables.
-We implemented an algorithm for _matching_ modulo AC, not for
-_unifying_ modulo AC. As a consequence, existential variables
-appearing in a goal are considered as constants, they will not be
-instantiated. *)
+(** *** Existential variables
+
+  We implemented an algorithm for _matching_ modulo AC, not for
+  _unifying_ modulo AC. As a consequence, existential variables
+  appearing in a goal are considered as constants, they will not be
+  instantiated. *)
 
 Section evars.
   Import ZArith.
@@ -220,7 +216,7 @@ Section evars.
 End evars.
 
 
-(** *** 3. Distinction between [aac_rewrite] and [aacu_rewrite] *)
+(** *** Distinction between [aac_rewrite] and [aacu_rewrite] *)
 
 Section U.
   Context {X} {R} {E: @Equivalence X R}
@@ -255,7 +251,7 @@ Section U.
 
 End U.
 
-(** *** 4. Rewriting units *)
+(** *** Rewriting units *)
 Section V.
   Context {X} {R} {E: @Equivalence X R}
   {dot}  {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot}
@@ -283,8 +279,9 @@ Section V.
   Qed.
 End V.
 
-(** *** 5. Rewriting too much things.  *)
+(** *** Rewriting too many things  *)
 Section W.
+  Import Instances.Peano.
   Variables a b c: nat.
   Hypothesis H: 0 = c.
 
@@ -308,8 +305,9 @@ Section W.
 
 End W.
 
-(** *** 6. Rewriting nullifiable patterns.  *)
+(** *** Rewriting nullifiable patterns *)
 Section Z.
+  Import Instances.Peano.
 
 (** If the pattern of the rewritten hypothesis does not contain "hard"
 symbols (like constants, function symbols, AC or A symbols without
@@ -335,14 +333,12 @@ Goal a+b*c = c.
      *)
 Abort.
 
-(** **** If the pattern is a unit or can be instantiated to be equal
-   to a unit:
+(** *** If the pattern is a unit or can be instantiated to be equal to a unit
   
    The heuristic is to make the unit appear at each possible position
    in the term, e.g. transforming [a] into [1*a] and [a*1], but this
    process is not recursive (we will not transform [1*a]) into
    [(1+0*1)*a] *)
-
 Goal a+b+c = c.
  
   aac_instances H0 [mult].            
@@ -352,7 +348,10 @@ Goal a+b+c = c.
   (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*)
 Abort.
 
-(** *** Another example of the former case is the following, where the hypothesis can be instantiated to be equal to [1] *)
+(** *** Another example of the former case
+ 
+  In the following, the hypothesis can be instantiated
+  to be equal to [1]. *)
 Hypothesis H : forall x y, (x+y)*x = x*x + y *x.
 Goal a*a+b*a + c = c.
   (** Here, only one solution if we use the aac_instance tactic  *)
@@ -371,4 +370,3 @@ still unclear how to handle properly this kind of situation : we plan
 to investigate on this in the future *)
 
 End Z.
-
diff --git a/theories/Constants.v b/theories/Constants.v
index 356d803..ca40094 100644
--- a/theories/Constants.v
+++ b/theories/Constants.v
@@ -13,15 +13,15 @@ Register Init.Datatypes.list as aac_tactics.list.typ.
 Register Init.Datatypes.nil as aac_tactics.list.nil.
 Register Init.Datatypes.cons as aac_tactics.list.cons.
 
-Require BinNums.
+From Coq Require BinNums.
 Register BinNums.positive as aac_tactics.pos.typ.
 Register BinNums.xI as aac_tactics.pos.xI.
 Register BinNums.xO as aac_tactics.pos.xO.
 Register BinNums.xH as aac_tactics.pos.xH.
 
-Require Coq.Classes.Morphisms.
+From Coq Require Classes.Morphisms.
 Register Morphisms.Proper as aac_tactics.coq.classes.morphisms.Proper.
-Require Coq.Classes.RelationClasses.
+From Coq Require Classes.RelationClasses.
 
 Register RelationClasses.Equivalence as aac_tactics.coq.RelationClasses.Equivalence.
 Register RelationClasses.Reflexive as aac_tactics.coq.RelationClasses.Reflexive.
diff --git a/theories/Instances.v b/theories/Instances.v
index ac8d747..08dc14a 100644
--- a/theories/Instances.v
+++ b/theories/Instances.v
@@ -6,198 +6,225 @@
 (*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
 (***************************************************************************)
 
-Require List.
-Require PeanoNat NArith.
-Require ZArith Zminmax.
-Require QArith Qminmax.
-Require Relations.
-
-From AAC_tactics
-Require Export AAC.
-
-(** Instances for aac_rewrite.*)
+(** * Instances for AAC Tactics *)
 
+From Coq Require PeanoNat ZArith Zminmax NArith List Permutation.
+From Coq Require QArith Qminmax Relations.
+From AAC_tactics Require Export AAC.
 
 (* This one is not declared as an instance: this interferes badly with setoid_rewrite *)
 Lemma eq_subr {X} {R} `{@Reflexive X R}: subrelation eq R.
 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.
   Import PeanoNat.
-  #[global] Instance aac_add_Assoc : Associative eq Nat.add := Nat.add_assoc.
-  #[global] Instance aac_add_Comm : Commutative eq Nat.add := Nat.add_comm.
+  #[export] Instance aac_add_Assoc : Associative eq Nat.add := Nat.add_assoc.
+  #[export] Instance aac_add_Comm : Commutative eq Nat.add := Nat.add_comm.
 
-  #[global] Instance aac_mult_Comm : Commutative eq Nat.mul := Nat.mul_comm.
-  #[global] Instance aac_mult_Assoc : Associative eq Nat.mul := Nat.mul_assoc.
+  #[export] Instance aac_mul_Comm : Commutative eq Nat.mul := Nat.mul_comm.
+  #[export] Instance aac_mul_Assoc : Associative eq Nat.mul := Nat.mul_assoc.
  
-  #[global] Instance aac_min_Comm : Commutative eq Nat.min := Nat.min_comm.
-  #[global] Instance aac_min_Assoc : Associative eq Nat.min := Nat.min_assoc.
-  #[global] Instance aac_min_Idem : Idempotent eq Nat.min := Nat.min_idempotent.
+  #[export] Instance aac_min_Comm : Commutative eq Nat.min := Nat.min_comm.
+  #[export] Instance aac_min_Assoc : Associative eq Nat.min := Nat.min_assoc.
+  #[export] Instance aac_min_Idem : Idempotent eq Nat.min := Nat.min_idempotent.
 
-  #[global] Instance aac_max_Comm : Commutative eq Nat.max := Nat.max_comm.
-  #[global] Instance aac_max_Assoc : Associative eq Nat.max := Nat.max_assoc.
-  #[global] Instance aac_max_Idem : Idempotent eq Nat.max := Nat.max_idempotent.
+  #[export] Instance aac_max_Comm : Commutative eq Nat.max := Nat.max_comm.
+  #[export] Instance aac_max_Assoc : Associative eq Nat.max := Nat.max_assoc.
+  #[export] Instance aac_max_Idem : Idempotent eq Nat.max := Nat.max_idempotent.
  
-  #[global] Instance aac_one : Unit eq Nat.mul 1 := Build_Unit eq Nat.mul 1 Nat.mul_1_l Nat.mul_1_r. 
-  #[global] Instance aac_zero_add : Unit eq Nat.add O := Build_Unit eq Nat.add (O) Nat.add_0_l Nat.add_0_r.
-  #[global] Instance aac_zero_max : Unit eq Nat.max  O := Build_Unit eq Nat.max 0 Nat.max_0_l Nat.max_0_r. 
-
+  #[export] Instance aac_one : Unit eq Nat.mul 1 :=
+    Build_Unit eq Nat.mul 1 Nat.mul_1_l Nat.mul_1_r.
+  #[export] Instance aac_zero_add : Unit eq Nat.add O :=
+    Build_Unit eq Nat.add (O) Nat.add_0_l Nat.add_0_r.
+  #[export] Instance aac_zero_max : Unit eq Nat.max  O :=
+    Build_Unit eq Nat.max 0 Nat.max_0_l Nat.max_0_r.
 
   (* We also provide liftings from le to eq *)
-  #[global] Instance preorder_le : PreOrder le := Build_PreOrder _ Nat.le_refl Nat.le_trans.
-  #[global] Instance lift_le_eq : AAC_lift le eq := Build_AAC_lift eq_equivalence _.
-
+  #[export] Instance preorder_le : PreOrder le :=
+    Build_PreOrder _ Nat.le_refl Nat.le_trans.
+  #[export] Instance lift_le_eq : AAC_lift le eq :=
+    Build_AAC_lift eq_equivalence _.
 End Peano.
 
-
 Module Z.
   Import ZArith Zminmax.
   Open Scope Z_scope.
-  #[global] Instance aac_Zplus_Assoc : Associative eq Zplus :=  Zplus_assoc.
-  #[global] Instance aac_Zplus_Comm : Commutative eq Zplus :=  Zplus_comm.
+  #[export] Instance aac_Zplus_Assoc : Associative eq Zplus :=  Zplus_assoc.
+  #[export] Instance aac_Zplus_Comm : Commutative eq Zplus :=  Zplus_comm.
  
-  #[global] Instance aac_Zmult_Comm : Commutative eq Zmult :=  Zmult_comm.
-  #[global] Instance aac_Zmult_Assoc : Associative eq Zmult :=  Zmult_assoc.
+  #[export] Instance aac_Zmult_Comm : Commutative eq Zmult :=  Zmult_comm.
+  #[export] Instance aac_Zmult_Assoc : Associative eq Zmult :=  Zmult_assoc.
  
-  #[global] Instance aac_Zmin_Comm : Commutative eq Z.min :=  Z.min_comm.
-  #[global] Instance aac_Zmin_Assoc : Associative eq Z.min :=  Z.min_assoc.
-  #[global] Instance aac_Zmin_Idem : Idempotent eq Z.min :=  Z.min_idempotent.
+  #[export] Instance aac_Zmin_Comm : Commutative eq Z.min :=  Z.min_comm.
+  #[export] Instance aac_Zmin_Assoc : Associative eq Z.min :=  Z.min_assoc.
+  #[export] Instance aac_Zmin_Idem : Idempotent eq Z.min :=  Z.min_idempotent.
 
-  #[global] Instance aac_Zmax_Comm : Commutative eq Z.max :=  Z.max_comm.
-  #[global] Instance aac_Zmax_Assoc : Associative eq Z.max :=  Z.max_assoc.
-  #[global] Instance aac_Zmax_Idem : Idempotent eq Z.max :=  Z.max_idempotent.
+  #[export] Instance aac_Zmax_Comm : Commutative eq Z.max :=  Z.max_comm.
+  #[export] Instance aac_Zmax_Assoc : Associative eq Z.max :=  Z.max_assoc.
+  #[export] Instance aac_Zmax_Idem : Idempotent eq Z.max :=  Z.max_idempotent.
  
-  #[global] Instance aac_one : Unit eq Zmult 1 :=  Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. 
-  #[global] Instance aac_zero_Zplus  : Unit eq Zplus 0 := Build_Unit eq Zplus 0 Zplus_0_l Zplus_0_r.
+  #[export] Instance aac_one : Unit eq Zmult 1 :=
+    Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. 
+  #[export] Instance aac_zero_Zplus : Unit eq Zplus 0 :=
+    Build_Unit eq Zplus 0 Zplus_0_l Zplus_0_r.
 
   (* We also provide liftings from le to eq *)
-  #[global] Instance preorder_Zle : PreOrder Z.le := Build_PreOrder _ Z.le_refl Z.le_trans.
-  #[global] Instance lift_le_eq : AAC_lift Z.le eq := Build_AAC_lift eq_equivalence _.
-
+  #[export] Instance preorder_Zle : PreOrder Z.le :=
+    Build_PreOrder _ Z.le_refl Z.le_trans.
+  #[export] Instance lift_le_eq : AAC_lift Z.le eq :=
+    Build_AAC_lift eq_equivalence _.
 End Z.
 
 Module Lists.
-   Import List.
-  #[global] Instance aac_append_Assoc {A} : Associative eq (@app A) := @app_assoc A.
-  #[global] Instance aac_nil_append  {A} : @Unit (list A) eq (@app A) (@nil A) := Build_Unit _ (@app A) (@nil A) (@app_nil_l A) (@app_nil_r A).
-  #[global] Instance aac_append_Proper {A} : Proper (eq ==> eq ==> eq) (@app A).
-   Proof.
-     repeat intro.
-     subst.
-     reflexivity.
-   Qed.
+  Import List Permutation.
+  #[export] Instance aac_append_Assoc {A} : Associative eq (@app A) := @app_assoc A.
+  #[export] Instance aac_nil_append  {A} : Unit eq (@app A) (@nil A) :=
+    Build_Unit _ (@app A) (@nil A) (@app_nil_l A) (@app_nil_r A).
+  #[export] Instance aac_append_Proper {A} : Proper (eq ==> eq ==> eq) (@app A).
+  Proof. repeat intro; subst; reflexivity. Qed.
+
+  #[export] Instance aac_append_Permutation_Assoc {A} : Associative (@Permutation A) (@app A).
+  Proof. repeat intro; rewrite app_assoc; apply Permutation_refl. Qed.
+  #[export] Instance aac_append_Permutation_Comm {A} : Commutative (@Permutation A) (@app A) :=
+    @Permutation_app_comm A.
+  #[export] Instance aac_nil_Permutation_append {A} : Unit (@Permutation A) (@app A) (@nil A) :=
+    Build_Unit (@Permutation A) (@app A) (@nil A) (fun x => Permutation_refl x)
+     (fun x => eq_ind_r (fun l => Permutation l _) (Permutation_refl x) (app_nil_r x)).
 End Lists.
 
-
 Module N.
   Import NArith.
   Open Scope N_scope.
-  #[global] Instance aac_Nplus_Assoc : Associative eq Nplus :=  Nplus_assoc.
-  #[global] Instance aac_Nplus_Comm : Commutative eq Nplus :=  Nplus_comm.
+  #[export] Instance aac_Nplus_Assoc : Associative eq Nplus :=  Nplus_assoc.
+  #[export] Instance aac_Nplus_Comm : Commutative eq Nplus :=  Nplus_comm.
  
-  #[global] Instance aac_Nmult_Comm : Commutative eq Nmult :=  Nmult_comm.
-  #[global] Instance aac_Nmult_Assoc : Associative eq Nmult :=  Nmult_assoc.
+  #[export] Instance aac_Nmult_Comm : Commutative eq Nmult :=  Nmult_comm.
+  #[export] Instance aac_Nmult_Assoc : Associative eq Nmult :=  Nmult_assoc.
  
-  #[global] Instance aac_Nmin_Comm : Commutative eq N.min :=  N.min_comm.
-  #[global] Instance aac_Nmin_Assoc : Associative eq N.min :=  N.min_assoc.
-  #[global] Instance aac_Nmin_Idem : Idempotent eq N.min :=  N.min_idempotent.
+  #[export] Instance aac_Nmin_Comm : Commutative eq N.min :=  N.min_comm.
+  #[export] Instance aac_Nmin_Assoc : Associative eq N.min :=  N.min_assoc.
+  #[export] Instance aac_Nmin_Idem : Idempotent eq N.min :=  N.min_idempotent.
 
-  #[global] Instance aac_Nmax_Comm : Commutative eq N.max :=  N.max_comm.
-  #[global] Instance aac_Nmax_Assoc : Associative eq N.max :=  N.max_assoc.
-  #[global] Instance aac_Nmax_Idem : Idempotent eq N.max :=  N.max_idempotent.
+  #[export] Instance aac_Nmax_Comm : Commutative eq N.max :=  N.max_comm.
+  #[export] Instance aac_Nmax_Assoc : Associative eq N.max :=  N.max_assoc.
+  #[export] Instance aac_Nmax_Idem : Idempotent eq N.max :=  N.max_idempotent.
  
-  #[global] Instance aac_one  : Unit eq Nmult (1)%N := Build_Unit eq Nmult (1)%N Nmult_1_l Nmult_1_r. 
-  #[global] Instance aac_zero  : Unit eq Nplus (0)%N := Build_Unit eq Nplus (0)%N Nplus_0_l Nplus_0_r.
-  #[global] Instance aac_zero_max  :  Unit eq N.max 0 := Build_Unit eq N.max 0 N.max_0_l N.max_0_r. 
+  #[export] Instance aac_one  : Unit eq Nmult (1)%N :=
+    Build_Unit eq Nmult (1)%N Nmult_1_l Nmult_1_r. 
+  #[export] Instance aac_zero  : Unit eq Nplus (0)%N :=
+    Build_Unit eq Nplus (0)%N Nplus_0_l Nplus_0_r.
+  #[export] Instance aac_zero_max : Unit eq N.max 0 :=
+    Build_Unit eq N.max 0 N.max_0_l N.max_0_r.
    
   (* We also provide liftings from le to eq *)
-  #[global] Instance preorder_le : PreOrder N.le := Build_PreOrder N.le N.le_refl N.le_trans.
-  #[global] Instance lift_le_eq : AAC_lift N.le eq := Build_AAC_lift eq_equivalence _.
-
+  #[export] Instance preorder_le : PreOrder N.le :=
+    Build_PreOrder N.le N.le_refl N.le_trans.
+  #[export] Instance lift_le_eq : AAC_lift N.le eq :=
+    Build_AAC_lift eq_equivalence _.
 End N.
 
 Module P.
   Import NArith.
   Open Scope positive_scope.
-  #[global] Instance aac_Pplus_Assoc : Associative eq Pplus :=  Pplus_assoc.
-  #[global] Instance aac_Pplus_Comm : Commutative eq Pplus :=  Pplus_comm.
+  #[export] Instance aac_Pplus_Assoc : Associative eq Pplus :=  Pplus_assoc.
+  #[export] Instance aac_Pplus_Comm : Commutative eq Pplus :=  Pplus_comm.
  
-  #[global]
-  Instance aac_Pmult_Comm : Commutative eq Pmult :=  Pmult_comm.
-  #[global] Instance aac_Pmult_Assoc : Associative eq Pmult :=  Pmult_assoc.
+  #[export] Instance aac_Pmult_Comm : Commutative eq Pmult :=  Pmult_comm.
+  #[export] Instance aac_Pmult_Assoc : Associative eq Pmult :=  Pmult_assoc.
  
-  #[global] Instance aac_Pmin_Comm : Commutative eq Pos.min :=  Pos.min_comm.
-  #[global] Instance aac_Pmin_Assoc : Associative eq Pos.min :=  Pos.min_assoc.
-  #[global] Instance aac_Pmin_Idem : Idempotent eq Pos.min :=  Pos.min_idempotent.
+  #[export] Instance aac_Pmin_Comm : Commutative eq Pos.min :=  Pos.min_comm.
+  #[export] Instance aac_Pmin_Assoc : Associative eq Pos.min :=  Pos.min_assoc.
+  #[export] Instance aac_Pmin_Idem : Idempotent eq Pos.min :=  Pos.min_idempotent.
 
-  #[global] Instance aac_Pmax_Comm : Commutative eq Pos.max :=  Pos.max_comm.
-  #[global] Instance aac_Pmax_Assoc : Associative eq Pos.max :=  Pos.max_assoc.
-  #[global] Instance aac_Pmax_Idem : Idempotent eq Pos.max :=  Pos.max_idempotent.
+  #[export] Instance aac_Pmax_Comm : Commutative eq Pos.max :=  Pos.max_comm.
+  #[export] Instance aac_Pmax_Assoc : Associative eq Pos.max :=  Pos.max_assoc.
+  #[export] Instance aac_Pmax_Idem : Idempotent eq Pos.max :=  Pos.max_idempotent.
 
-  (*  TODO : add this lemma in the stdlib *)
+  (* TODO: add this lemma in the stdlib *)
   Lemma Pmult_1_l (x : positive) : 1 * x = x.
   Proof. reflexivity. Qed.
 
-  #[global] Instance aac_one  : Unit eq Pmult 1 := Build_Unit eq Pmult 1 Pmult_1_l Pmult_1_r.
-  #[global] Instance aac_one_max  :  Unit eq Pos.max 1 := Build_Unit eq Pos.max 1 Pos.max_1_l Pos.max_1_r. 
+  #[export] Instance aac_one : Unit eq Pmult 1 :=
+    Build_Unit eq Pmult 1 Pmult_1_l Pmult_1_r.
+  #[export] Instance aac_one_max : Unit eq Pos.max 1 :=
+    Build_Unit eq Pos.max 1 Pos.max_1_l Pos.max_1_r.
 
   (* We also provide liftings from le to eq *)
-  #[global] Instance preorder_le : PreOrder Pos.le := Build_PreOrder Pos.le Pos.le_refl Pos.le_trans.
-  #[global] Instance lift_le_eq : AAC_lift Pos.le eq := Build_AAC_lift eq_equivalence _.
+  #[export] Instance preorder_le : PreOrder Pos.le :=
+    Build_PreOrder Pos.le Pos.le_refl Pos.le_trans.
+  #[export] Instance lift_le_eq : AAC_lift Pos.le eq :=
+    Build_AAC_lift eq_equivalence _.
 End P.
 
 Module Q.
   Import QArith Qminmax.
-  #[global] Instance aac_Qplus_Assoc : Associative Qeq Qplus :=  Qplus_assoc.
-  #[global] Instance aac_Qplus_Comm : Commutative Qeq Qplus :=  Qplus_comm.
+  #[export] Instance aac_Qplus_Assoc : Associative Qeq Qplus := Qplus_assoc.
+  #[export] Instance aac_Qplus_Comm : Commutative Qeq Qplus := Qplus_comm.
  
-  #[global] Instance aac_Qmult_Comm : Commutative Qeq Qmult :=  Qmult_comm.
-  #[global] Instance aac_Qmult_Assoc : Associative Qeq Qmult :=  Qmult_assoc.
+  #[export] Instance aac_Qmult_Comm : Commutative Qeq Qmult := Qmult_comm.
+  #[export] Instance aac_Qmult_Assoc : Associative Qeq Qmult := Qmult_assoc.
  
-  #[global] Instance aac_Qmin_Comm : Commutative Qeq Qmin :=  Q.min_comm.
-  #[global] Instance aac_Qmin_Assoc : Associative Qeq Qmin :=  Q.min_assoc.
-  #[global] Instance aac_Qmin_Idem : Idempotent Qeq Qmin :=  Q.min_idempotent.
+  #[export] Instance aac_Qmin_Comm : Commutative Qeq Qmin := Q.min_comm.
+  #[export] Instance aac_Qmin_Assoc : Associative Qeq Qmin := Q.min_assoc.
+  #[export] Instance aac_Qmin_Idem : Idempotent Qeq Qmin := Q.min_idempotent.
 
-  #[global] Instance aac_Qmax_Comm : Commutative Qeq Qmax :=  Q.max_comm.
-  #[global] Instance aac_Qmax_Assoc : Associative Qeq Qmax :=  Q.max_assoc.
-  #[global] Instance aac_Qmax_Idem : Idempotent Qeq Qmax :=  Q.max_idempotent.
+  #[export] Instance aac_Qmax_Comm : Commutative Qeq Qmax := Q.max_comm.
+  #[export] Instance aac_Qmax_Assoc : Associative Qeq Qmax := Q.max_assoc.
+  #[export] Instance aac_Qmax_Idem : Idempotent Qeq Qmax := Q.max_idempotent.
  
-  #[global] Instance aac_one : Unit Qeq Qmult 1 :=  Build_Unit Qeq Qmult 1 Qmult_1_l Qmult_1_r. 
-  #[global] Instance aac_zero_Qplus  : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r.
+  #[export] Instance aac_one : Unit Qeq Qmult 1 := 
+    Build_Unit Qeq Qmult 1 Qmult_1_l Qmult_1_r. 
+  #[export] Instance aac_zero_Qplus  : Unit Qeq Qplus 0 :=
+    Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r.
 
   (* We also provide liftings from le to eq *)
-  #[global] Instance preorder_le : PreOrder Qle := Build_PreOrder Qle Qle_refl Qle_trans.
-  #[global] Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _.
-
+  #[export] Instance preorder_le : PreOrder Qle :=
+    Build_PreOrder Qle Qle_refl Qle_trans.
+  #[export] Instance lift_le_eq : AAC_lift Qle Qeq :=
+    Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _.
 End Q.
 
 Module Prop_ops.
-  #[global] Instance aac_or_Assoc : Associative iff or. Proof.  unfold Associative; tauto.  Qed.
-  #[global] Instance aac_or_Comm : Commutative iff or. Proof.  unfold Commutative; tauto.  Qed.
-  #[global] Instance aac_or_Idem : Idempotent iff or. Proof.  unfold Idempotent; tauto.  Qed.
-  #[global] Instance aac_and_Idem : Idempotent iff and. Proof.  unfold Idempotent; tauto.  Qed.
-  #[global] Instance aac_True : Unit iff or False.  Proof.  constructor; firstorder.  Qed.
-  #[global] Instance aac_False : Unit iff and True.  Proof.  constructor; firstorder.  Qed.
+  #[export] Instance aac_or_Assoc : Associative iff or.
+  Proof. unfold Associative; tauto. Qed.
+  #[export] Instance aac_or_Comm : Commutative iff or.
+  Proof. unfold Commutative; tauto. Qed.
+  #[export] Instance aac_or_Idem : Idempotent iff or.
+  Proof. unfold Idempotent; tauto. Qed.
+  #[export] Instance aac_and_Idem : Idempotent iff and.
+  Proof. unfold Idempotent; tauto. Qed.
+  #[export] Instance aac_True : Unit iff or False.
+  Proof. constructor; firstorder. Qed.
+  #[export] Instance aac_False : Unit iff and True.
+  Proof. constructor; firstorder. Qed.
  
-  #[global] Program Instance aac_not_compat : Proper (iff ==> iff) not.
-  Solve All Obligations with firstorder.
+  #[export] Program Instance aac_not_compat : Proper (iff ==> iff) not.
 
-  #[global] Instance lift_impl_iff : AAC_lift Basics.impl iff := Build_AAC_lift _  _.
+  Solve All Obligations with firstorder.
+  #[export] Instance lift_impl_iff : AAC_lift Basics.impl iff :=
+    Build_AAC_lift _  _.
 End Prop_ops.
 
 Module Bool.
-  #[global] Instance aac_orb_Assoc : Associative eq orb. Proof.  unfold Associative; firstorder with bool.  Qed.
-  #[global] Instance aac_orb_Comm : Commutative eq orb. Proof.  unfold Commutative; firstorder with bool.  Qed.
-  #[global] Instance aac_orb_Idem : Idempotent eq orb. Proof.  intro; apply Bool.orb_diag.  Qed.
-  #[global] Instance aac_andb_Assoc : Associative eq andb. Proof.  unfold Associative; firstorder with bool.  Qed.
-  #[global] Instance aac_andb_Comm : Commutative eq andb. Proof.  unfold Commutative; firstorder with bool.  Qed.
-  #[global] Instance aac_andb_Idem : Idempotent eq andb. Proof.  intro; apply Bool.andb_diag.  Qed.
-  #[global] Instance aac_true : Unit eq orb false.  Proof.  constructor; firstorder with bool.  Qed.
-  #[global] Instance aac_false : Unit eq andb true.  Proof.  constructor; intros [|];firstorder.  Qed.
+  #[export] Instance aac_orb_Assoc : Associative eq orb.
+  Proof. unfold Associative; firstorder with bool. Qed.
+  #[export] Instance aac_orb_Comm : Commutative eq orb.
+  Proof. unfold Commutative; firstorder with bool. Qed.
+  #[export] Instance aac_orb_Idem : Idempotent eq orb.
+  Proof. intro; apply Bool.orb_diag. Qed.
+  #[export] Instance aac_andb_Assoc : Associative eq andb.
+  Proof. unfold Associative; firstorder with bool. Qed.
+  #[export] Instance aac_andb_Comm : Commutative eq andb.
+  Proof. unfold Commutative; firstorder with bool. Qed.
+  #[export] Instance aac_andb_Idem : Idempotent eq andb.
+  Proof. intro; apply Bool.andb_diag. Qed.
+  #[export] Instance aac_true : Unit eq orb false.
+  Proof. constructor; firstorder with bool. Qed.
+  #[export] Instance aac_false : Unit eq andb true.
+  Proof. constructor; intros [|]; firstorder. Qed.
  
-  #[global] Instance negb_compat : Proper (eq ==> eq) negb.  Proof. intros [|] [|]; auto. Qed.
+  #[export] Instance negb_compat : Proper (eq ==> eq) negb.
+  Proof. intros [|] [|]; auto. Qed.
 End Bool.
 
 Module Relations.
@@ -214,58 +241,62 @@ Module Relations.
     Definition top : relation T := fun _ _ => True.
   End defs.
  
-  #[global] Instance eq_same_relation T : Equivalence (same_relation T). Proof. firstorder. Qed.
+  #[export] Instance eq_same_relation T : Equivalence (same_relation T).
+  Proof. firstorder. Qed.
  
-  #[global]
-  Instance aac_union_Comm T : Commutative (same_relation T) (union T). Proof. unfold Commutative; compute; intuition.  Qed.
-  #[global] Instance aac_union_Assoc T : Associative (same_relation T) (union T). Proof. unfold Associative; compute; intuition.  Qed.
-  #[global] Instance aac_union_Idem T : Idempotent (same_relation T) (union T). Proof. unfold Idempotent; compute; intuition.  Qed.
-  #[global] Instance aac_bot T : Unit (same_relation T) (union T) (bot T). Proof. constructor; compute; intuition. Qed.
-
-  #[global] Instance aac_inter_Comm T : Commutative (same_relation T) (inter T). Proof. unfold Commutative; compute; intuition.  Qed.
-  #[global] Instance aac_inter_Assoc T : Associative (same_relation T) (inter T). Proof. unfold Associative; compute; intuition.  Qed.
-  #[global] Instance aac_inter_Idem T : Idempotent (same_relation T) (inter T). Proof. unfold Idempotent; compute; intuition.  Qed.
-  #[global] Instance aac_top T : Unit (same_relation T) (inter T) (top T). Proof. constructor; compute; intuition. Qed.
+  #[export] Instance aac_union_Comm T : Commutative (same_relation T) (union T).
+  Proof. unfold Commutative; compute; intuition. Qed.
+  #[export] Instance aac_union_Assoc T : Associative (same_relation T) (union T).
+  Proof. unfold Associative; compute; intuition. Qed.
+  #[export] Instance aac_union_Idem T : Idempotent (same_relation T) (union T).
+  Proof. unfold Idempotent; compute; intuition. Qed.
+  #[export] Instance aac_bot T : Unit (same_relation T) (union T) (bot T).
+  Proof. constructor; compute; intuition. Qed.
+
+  #[export] Instance aac_inter_Comm T : Commutative (same_relation T) (inter T).
+  Proof. unfold Commutative; compute; intuition. Qed.
+  #[export] Instance aac_inter_Assoc T : Associative (same_relation T) (inter T).
+  Proof. unfold Associative; compute; intuition.  Qed.
+  #[export] Instance aac_inter_Idem T : Idempotent (same_relation T) (inter T).
+  Proof. unfold Idempotent; compute; intuition. Qed.
+  #[export] Instance aac_top T : Unit (same_relation T) (inter T) (top T).
+  Proof. constructor; compute; intuition. Qed.
  
   (* note that we use [eq] directly as a neutral element for composition *)
-  #[global] Instance aac_compo T : Associative (same_relation T) (compo T). Proof. unfold Associative; compute; firstorder. Qed.
-  #[global] Instance aac_eq T : Unit (same_relation T) (compo T) (eq). Proof.  compute; firstorder subst; trivial. Qed.
+  #[export] Instance aac_compo T : Associative (same_relation T) (compo T).
+  Proof. unfold Associative; compute; firstorder. Qed.
+  #[export] Instance aac_eq T : Unit (same_relation T) (compo T) (eq).
+  Proof. compute; firstorder subst; trivial. Qed.
 
-  #[global] Instance negr_compat T : Proper (same_relation T ==> same_relation T) (negr T).
+  #[export] Instance negr_compat T : Proper (same_relation T ==> same_relation T) (negr T).
   Proof. compute. firstorder. Qed.
 
-  #[global] Instance transp_compat T : Proper (same_relation T ==> same_relation T) (transp T).
+  #[export] Instance transp_compat T : Proper (same_relation T ==> same_relation T) (transp T).
   Proof. compute. firstorder. Qed.
 
-  #[global]
-  Instance clos_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_trans T).
+  #[export] Instance clos_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_trans T).
   Proof.
     intros  R S H x y Hxy. induction Hxy.
-      constructor 1. apply H. assumption.
-      econstructor 2; eauto 3.
+    constructor 1. apply H. assumption.
+    econstructor 2; eauto 3.
   Qed.
-  #[global]
-  Instance clos_trans_compat T: Proper (same_relation T ==> same_relation T) (clos_trans T).
+  #[export] Instance clos_trans_compat T: Proper (same_relation T ==> same_relation T) (clos_trans T).
   Proof. intros R S H; split; apply clos_trans_incr, H. Qed.
 
-  #[global]
-  Instance clos_refl_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_refl_trans T).
+  #[export] Instance clos_refl_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_refl_trans T).
   Proof.
     intros R S H x y Hxy. induction Hxy.
-      constructor 1. apply H. assumption.
-      constructor 2.
-      econstructor 3; eauto 3.
+    constructor 1. apply H. assumption.
+    constructor 2.
+    econstructor 3; eauto 3.
   Qed.
-  #[global]
-  Instance clos_refl_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_refl_trans T).
+  #[export] Instance clos_refl_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_refl_trans T).
   Proof. intros R S H; split; apply clos_refl_trans_incr, H. Qed.
 
-  #[global]
-  Instance preorder_inclusion T : PreOrder (inclusion T).
-  Proof. constructor; unfold Reflexive, Transitive, inclusion; intuition.   Qed.
+  #[export] Instance preorder_inclusion T : PreOrder (inclusion T).
+  Proof. constructor; unfold Reflexive, Transitive, inclusion; intuition. Qed.
 
-  #[global]
-  Program Instance lift_inclusion_same_relation T: AAC_lift (inclusion T) (same_relation T) :=
+  #[export] Program Instance lift_inclusion_same_relation T : AAC_lift (inclusion T) (same_relation T) :=
     Build_AAC_lift (eq_same_relation T) _.
   Next Obligation. firstorder. Qed.
 
@@ -274,13 +305,14 @@ End Relations.
 Module All.
   Export Peano.
   Export Z.
+  Export Lists.
   Export P.
   Export N.
   Export Prop_ops.
   Export Bool.
   Export Relations.
 End All.
- 
+
 (* Here, we should not see any instance of our classes.
    Print HintDb typeclass_instances.
 *)
diff --git a/theories/Tutorial.v b/theories/Tutorial.v
index d8aa971..b26cca3 100644
--- a/theories/Tutorial.v
+++ b/theories/Tutorial.v
@@ -6,14 +6,9 @@
 (*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
 (***************************************************************************)
 
-(** * Tutorial for using the [aac_tactics] library.
-
-   Depending on your installation, either modify the following two
-   lines, or add them to your .coqrc files, replacing "."  with the
-   path to the [aac_tactics] library. *)
-
-Require PeanoNat ZArith Lia.
+(** * Tutorial for using the AAC Tactics library *)
 
+From Coq Require PeanoNat ZArith List Permutation Lia.
 From AAC_tactics Require Import AAC.
 From AAC_tactics Require Instances.
 
@@ -249,12 +244,15 @@ End base.
 Section Peano.
   Import PeanoNat.
 
-  Instance aac_plus_Assoc : Associative eq Nat.add := Nat.add_assoc.
-  Instance aac_plus_Comm : Commutative eq Nat.add :=  Nat.add_comm.
+  Instance aac_add_Assoc : Associative eq Nat.add := Nat.add_assoc.
+  Instance aac_add_Comm : Commutative eq Nat.add :=  Nat.add_comm.
+
+  Instance aac_mul_Comm : Commutative eq Nat.mul := Nat.mul_comm.
+  Instance aac_mul_Assoc : Associative eq Nat.mul := Nat.mul_assoc.
 
   Instance aac_one : Unit eq Nat.mul 1 :=
     Build_Unit eq Nat.mul 1 Nat.mul_1_l Nat.mul_1_r.
-  Instance aac_zero_plus : Unit eq Nat.add O :=
+  Instance aac_zero_add : Unit eq Nat.add O :=
     Build_Unit eq Nat.add (O) Nat.add_0_l Nat.add_0_r.
 
   (** Two (or more) operations may share the same units: in the
@@ -264,9 +262,9 @@ Section Peano.
   Instance aac_max_Comm : Commutative eq Nat.max :=  Nat.max_comm.
   Instance aac_max_Assoc : Associative eq Nat.max := Nat.max_assoc.
 
-  (** Commutative operations may additionally be declared as idempotent
-      this does not change the behaviour of [aac_rewrite], but this enables more simplifications in 
-      [aac_normalise] and [aac_reflexivity]
+  (** Commutative operations may additionally be declared as idempotent.
+      This does not change the behaviour of [aac_rewrite], but this enables
+      more simplifications in [aac_normalise] and [aac_reflexivity].
    *)
   Instance aac_max_Idem : Idempotent eq Nat.max := Nat.max_idempotent.
 
@@ -278,13 +276,12 @@ Section Peano.
     aac_reflexivity.
   Qed.
 
-  (* here we use idempotency *)
+  (** Here, we use idempotency. *)
   Goal Nat.max (a + 0) a = a.
     aac_reflexivity.
   Qed.
    
   (** Furthermore, several operators can be mixed: *)
-
   Hypothesis H : forall x y z, Nat.max (x + y) (x + z) = x + Nat.max y z.
  
   Goal Nat.max (a + b) (c + (a * 1)) = Nat.max c b + a.
@@ -293,7 +290,6 @@ Section Peano.
   Goal Nat.max (a + b) (c + Nat.max (a*1+0) 0) = a + Nat.max b c.
     aac_instances H. aac_rewrite H. aac_reflexivity.
   Qed.
-
  
   (** *** Working with inequations
 
@@ -375,9 +371,6 @@ Section AAC_normalise.
   
 End AAC_normalise.
 
-
-
-
 (** ** Examples from the web page *)
 Section Examples.
 
@@ -434,4 +427,24 @@ Section Examples.
 
 End Examples.
 
+(** ** List examples *)
+Section Lists.
+  Import List Permutation.
+  Import Instances.Lists.
+
+  Variables (X : Type) (l1 l2 l3 : list X).
 
+  Goal l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
+    aac_reflexivity.
+  Qed.
+
+  Goal Permutation (l1 ++ l2) (l2 ++ l1).
+    aac_reflexivity.
+  Qed.
+
+  Hypothesis H : Permutation l1 l2.
+  Goal Permutation (l1 ++ l3) (l3 ++ l2).
+    aac_rewrite H.
+    aac_reflexivity.
+  Qed.
+End Lists.
diff --git a/theories/Utils.v b/theories/Utils.v
index 54452f1..8d70440 100644
--- a/theories/Utils.v
+++ b/theories/Utils.v
@@ -6,19 +6,20 @@
 (*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
 (***************************************************************************)
 
+(** * Utility functions and results *)
 
-Require Import Arith NArith.
-Require Import List.
-Require Import FMapPositive FMapFacts.
-Require Import RelationClasses Equality.
+From Coq Require Import Arith NArith List.
+From Coq Require Import FMapPositive FMapFacts RelationClasses Equality.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 
-(** * Utilities for positive numbers
-   which we use as:
-     - indices for morphisms and symbols
-     - multiplicity of terms in sums *)
+(** ** Utilities for positive numbers
+
+ We use positive numbers as:
+ - indices for morphisms and symbols
+ - multiplicity of terms in sums
+*)
 
 Notation idx := positive.
 
@@ -67,7 +68,7 @@ Proof. induction i; destruct j; simpl; try constructor; case (IHi j); intros; co
 Lemma idx_compare_reflect_eq: forall i j, idx_compare i j = Eq -> i=j.
 Proof. intros i j. case (pos_compare_weak_spec i j); intros; congruence. Qed.
 
-(** * Dependent types utilities *)
+(** ** Dependent types utilities *)
 
 Notation cast T H u := (eq_rect _ T u _ H).
 
@@ -97,7 +98,7 @@ Section dep.
 End dep.
 
 
-(** * Utilities about (non-empty) lists and multisets  *)
+(** ** Utilities about (non-empty) lists and multisets  *)
 
 #[universes(template)]
 Inductive nelist (A : Type) : Type :=