switched to ssreflect 1.6

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
 
 
 

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

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.
+Qed.
+
+(* Local Variables: *)
+(* coq-load-path: (("." "Plain") ("../../theories" "Autosubst")) *)
+(* End: *)

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)

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: *)

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.

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.

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.

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.

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 :=

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 *)

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.

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.

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.