diff --git a/README.md b/README.md
index 8c964ad..6d5499e 100644
--- a/README.md
+++ b/README.md
@@ -8,8 +8,8 @@ https://www.ps.uni-saarland.de/autosubst
 
 ## Requirements
 
-- Coq 8.4 or Coq 8.5beta3
-- ssreflect version 1.4 or 1.5 for some examples
+- Coq 8.4 or Coq 8.5rc1
+- ssreflect version 1.6 for some examples
 
 
 
diff --git a/examples/plain/Context.v b/examples/plain/Context.v
index 40944a9..949c9be 100644
--- a/examples/plain/Context.v
+++ b/examples/plain/Context.v
@@ -1,6 +1,6 @@
 (** * Context *)
 Require Import Omega List Program.Equality.
-Require Import Autosubst.
+Require Import Autosubst.Autosubst.
 
 Fixpoint atn {X} l n (x : X) :=
   match l with
diff --git a/examples/plain/Demo.v b/examples/plain/Demo.v
index 440ea66..5c7ca2b 100644
--- a/examples/plain/Demo.v
+++ b/examples/plain/Demo.v
@@ -2,7 +2,7 @@
 
     In this tutorial we will use Autosubst to formalize the simply typed lambda calculus and show substitutivity and type preservation of the reduction relation. *)
 
-Require Import Autosubst.
+Require Import Autosubst.Autosubst.
 
 (** ** Syntax and the substitution operation
 
@@ -187,4 +187,8 @@ Proof.
   inversion H_step; ainv; eauto using ty.
   - eapply ty_subst; try eassumption.
     intros [|]; simpl; eauto using ty.
-Qed.
\ No newline at end of file
+Qed.
+
+(* Local Variables: *)
+(* coq-load-path: (("." "Plain") ("../../theories" "Autosubst")) *)
+(* End: *)
diff --git a/examples/plain/POPLmark.v b/examples/plain/POPLmark.v
index 36fc869..5c2c91c 100644
--- a/examples/plain/POPLmark.v
+++ b/examples/plain/POPLmark.v
@@ -6,7 +6,8 @@
     progress and preservation of System F with subtyping.  *)
 
 Require Import Program.Equality List Omega.
-Require Import Autosubst Size Decidable Context.
+Require Import Autosubst.Autosubst.
+Require Import Size Decidable Context.
 
 Inductive type : Type :=
 | TyVar (x : var)
diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index 76ce95d..7ff7871 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -1,6 +1,6 @@
 (** * Support for Size Induction *)
 Require Import Omega List Program.Equality.
-Require Import Autosubst_Basics.
+Require Import Autosubst.Autosubst_Basics.
 
 Class Size (A : Type) := size : A -> nat.
 
@@ -111,5 +111,5 @@ Instance size_fact_In (A : Type) (size_A : Size A) x l (x_in_l : In x l) :
 Proof. now apply size_In. Qed.
 
 (* Local Variables: *)
-(* coq-load-path: (("." "Plain")) *)
+(* coq-load-path: (("." "Plain") ("../../theories" "Autosubst")) *)
 (* End: *)
diff --git a/examples/ssr/ARS.v b/examples/ssr/ARS.v
index b7c1d04..3a1f6dc 100644
--- a/examples/ssr/ARS.v
+++ b/examples/ssr/ARS.v
@@ -1,7 +1,8 @@
 (** * Abstract Reduction Systems
 
     Useful lemmas when working with small-step reduction relations. *)
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/examples/ssr/AutosubstSsr.v b/examples/ssr/AutosubstSsr.v
index 4a56808..c18cd66 100644
--- a/examples/ssr/AutosubstSsr.v
+++ b/examples/ssr/AutosubstSsr.v
@@ -5,7 +5,8 @@ Require Export Autosubst_Classes.
 Require Export Autosubst_Tactics.
 Require Export Autosubst_Lemmas.
 Require Export Autosubst_Derive.
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/examples/ssr/BetaSubstitution.v b/examples/ssr/BetaSubstitution.v
index b65e940..1b0b748 100644
--- a/examples/ssr/BetaSubstitution.v
+++ b/examples/ssr/BetaSubstitution.v
@@ -1,5 +1,6 @@
 (** * Correctness of Single Variable Substitutions *)
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import Autosubst.
 
 Set Implicit Arguments.
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 549c40e..d1d09cc 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -1,4 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import AutosubstSsr ARS.
 
 Set Implicit Arguments.
diff --git a/examples/ssr/Context.v b/examples/ssr/Context.v
index 40b3733..d0bb36e 100644
--- a/examples/ssr/Context.v
+++ b/examples/ssr/Context.v
@@ -1,7 +1,8 @@
 (** * Context
 
     Support for dependent contexts with the right reduction behaviour. *)
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import AutosubstSsr.
 
 Definition get {T} `{Ids T} (Gamma : seq T) (n : var) : T :=
diff --git a/examples/ssr/POPLmark.v b/examples/ssr/POPLmark.v
index d32e688..a0af0e7 100644
--- a/examples/ssr/POPLmark.v
+++ b/examples/ssr/POPLmark.v
@@ -9,7 +9,8 @@
     and in particular does not contain well-formedness assumptions.
  *)
 
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import AutosubstSsr Context.
 
 (** **** Syntax *)
diff --git a/examples/ssr/SystemF_CBV.v b/examples/ssr/SystemF_CBV.v
index 81b413f..b0f6c8b 100644
--- a/examples/ssr/SystemF_CBV.v
+++ b/examples/ssr/SystemF_CBV.v
@@ -1,6 +1,7 @@
 (** * Normalization of Call-By-Value System F *)
 
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import AutosubstSsr Context.
 
 Set Implicit Arguments.
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index 41c5228..a6440b8 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -1,5 +1,7 @@
 (** * Strong Normalization of System F *)
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import AutosubstSsr ARS Context.
 
 Set Implicit Arguments.
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index 56dfdab..585d2f8 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -1,7 +1,9 @@
 (** * Predicative CC omega: Type Preservation and Confluence
  *)
 
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import AutosubstSsr ARS Context.
 
 Set Implicit Arguments.