NixOS · Jul 11, 2017 · Jul 11, 2017 · Jul 11, 2017 · Jul 11, 2017
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -1,16 +1,16 @@
 {stdenv, fetchgit, coq, coqPackages}:
 
-let revision = "04785ee692036e7ba9f4c4e380b1995128a97bf8"; in
+let revision = "ee436635a34873c79f49c3d2d507194216f6e8e9"; in
 
 stdenv.mkDerivation rec {
 
   name = "coq-QuickChick-${coq.coq-version}-${version}";
-  version = "20170422-${builtins.substring 0 7 revision}";
+  version = "20170710-${builtins.substring 0 7 revision}";
 
   src = fetchgit {
     url = git://github.com/QuickChick/QuickChick.git;
     rev = revision;
-    sha256 = "1x5idk9d9r5mj1w54676a5j92wr1id7c9dmknkpmnh78rgrqzy5j";
+    sha256 = "0sq14j1kl4m4plyxj2dbkfwa6iqipmf9w7mxxxcbsm718m0xf1gr";
   };
 
   buildInputs = [ coq.ocaml coq.camlp5 ];

diff --git a/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch b/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch
@@ -0,0 +1,134 @@
+From 5b40a32e35fe446cda20ed34c756a010856f39ce Mon Sep 17 00:00:00 2001
+From: Theo Giannakopoulos <theo.giannakopoulos@baesystems.com>
+Date: Wed, 5 Apr 2017 15:48:55 -0400
+Subject: [PATCH] changes to work with Coq 8.6
+
+---
+ theories/Autosubst_Derive.v | 12 ++++++++++++
+ theories/Autosubst_MMap.v   |  3 ++-
+ 2 files changed, 14 insertions(+), 1 deletion(-)
+
+diff --git a/theories/Autosubst_Derive.v b/theories/Autosubst_Derive.v
+index 61995de..cf87f67 100644
+--- a/theories/Autosubst_Derive.v
++++ b/theories/Autosubst_Derive.v
+@@ -18,6 +18,7 @@ Hint Extern 0 (Ids _) => derive_Ids : derive.
+
+ Ltac derive_Rename :=
+   match goal with [ |- Rename ?term ] =>
++    let inst := fresh "inst" in
+     hnf; fix inst 2; change _ with (Rename term) in inst;
+     intros xi s; change (annot term s); destruct s;
+     match goal with
+@@ -66,6 +67,7 @@ Ltac has_var s :=
+ Ltac derive_Subst :=
+   match goal with [ |- Subst ?term ] =>
+     require_instance (Rename term);
++    let inst := fresh "inst" in
+     hnf; fix inst 2; change _ with (Subst term) in inst;
+     intros sigma s; change (annot term s); destruct s;
+     match goal with
+@@ -107,6 +109,7 @@ Hint Extern 0 (Subst _) => derive_Subst : derive.
+ Ltac derive_HSubst :=
+   match goal with [ |- HSubst ?inner ?outer ] =>
+     require_instance (Subst inner);
++    let inst := fresh "inst" in
+     hnf; fix inst 2; change _ with (HSubst inner outer) in inst;
+     intros sigma s; change (annot outer s); destruct s;
+     match goal with
+@@ -327,6 +330,7 @@ Ltac derive_SubstLemmas :=
+      assert (up_upren_n :
+                forall xi n, upn n (ren xi) = ren (iterate upren n xi)) by
+        (apply up_upren_n_internal, up_upren);
++     let ih := fresh "ih" in
+      fix ih 2; intros xi s; destruct s; try reflexivity; simpl; f_equal;
+      try apply mmap_ext; intros; rewrite ?up_upren, ?up_upren_n; apply ih);
+
+@@ -337,6 +341,7 @@ Ltac derive_SubstLemmas :=
+        (apply up_id_internal; reflexivity);
+      assert (up_id_n : forall n, upn n ids = ids) by
+        (apply up_id_n_internal, up_id);
++     let ih := fresh "ih" in
+      fix ih 1; intros s; destruct s; simpl; f_equal; try reflexivity;
+      rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; apply ih);
+
+@@ -344,6 +349,7 @@ Ltac derive_SubstLemmas :=
+
+     assert (ren_subst_comp :
+        forall xi sigma (s : term), (rename xi s).[sigma] = s.[xi >>> sigma]) by(
++     let ih := fresh "ih" in
+      fix ih 3; intros xi sigma s; destruct s; try reflexivity; simpl; f_equal;
+      rewrite ?up_comp_ren_subst, ?up_comp_ren_subst_n, ?mmap_comp;
+      try apply mmap_ext; intros; apply ih);
+@@ -357,6 +363,7 @@ Ltac derive_SubstLemmas :=
+      assert (up_comp_subst_ren_n :
+       forall sigma xi n, upn n (sigma >>> rename xi) = upn n sigma >>> rename (iterate upren n xi))
+       by (apply up_comp_subst_ren_n_internal; apply up_comp_subst_ren);
++     let ih := fresh "ih" in
+      fix ih 3; intros sigma xi s; destruct s; try reflexivity; simpl;
+      f_equal; rewrite ?up_comp_subst_ren, ?up_comp_subst_ren_n, ?mmap_comp;
+      try (rewrite hcomp_ren_internal; [|apply rename_subst]);
+@@ -368,6 +375,7 @@ Ltac derive_SubstLemmas :=
+       by (apply up_comp_internal; [reflexivity|apply ren_subst_comp|apply subst_ren_comp]);
+      assert (up_comp_n : forall sigma tau n, upn n (sigma >> tau) = upn n sigma >> upn n tau)
+       by (apply up_comp_n_internal; apply up_comp);
++     let ih := fresh "ih" in
+      fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal;
+      rewrite ?up_comp, ?up_comp_n, ?mmap_comp, ?hcomp_dist_internal;
+      try apply mmap_ext; intros; apply ih);
+@@ -382,6 +390,7 @@ Ltac derive_HSubstLemmas :=
+   let ids := constr:(ids : var -> inner) in
+
+   assert (hsubst_id : forall (s : outer), s.|[ids] = s) by (
++    let ih := fresh "ih" in
+     fix ih 1; intros s; destruct s; try reflexivity; simpl; f_equal;
+     rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros;
+     (apply subst_id || apply ih)
+@@ -390,6 +399,7 @@ Ltac derive_HSubstLemmas :=
+   assert (hsubst_comp : forall (theta eta : var -> inner) (s : outer),
+     s.|[theta].|[eta] = s.|[theta >> eta])
+   by (
++    let ih := fresh "ih" in
+     fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal;
+     rewrite <- ?up_comp, <- ?up_comp_n, ?mmap_comp; try apply mmap_ext; intros;
+     (apply subst_comp || apply ih)
+@@ -405,6 +415,7 @@ Ltac derive_SubstHSubstComp :=
+   assert (ren_hsubst_comp : forall xi (theta : var -> inner) (s : outer),
+     rename xi s.|[theta] = (rename xi s).|[theta]
+   ) by (
++    let ih := fresh "ih" in
+     fix ih 3; intros xi theta s; destruct s; try reflexivity; simpl; f_equal;
+     rewrite ?mmap_comp; try apply mmap_ext; intros; simpl; apply ih
+   );
+@@ -421,6 +432,7 @@ Ltac derive_SubstHSubstComp :=
+     apply up_hcomp_n_internal; apply up_hcomp
+   );
+
++  let ih := fresh "ih" in
+   fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal;
+   rewrite ?up_hcomp, ?up_hcomp_n, ?hcomp_lift_n_internal, ?mmap_comp;
+   try apply mmap_ext; intros; apply ih
+diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
+index f8387e7..7af7902 100644
+--- a/theories/Autosubst_MMap.v
++++ b/theories/Autosubst_MMap.v
+@@ -23,7 +23,7 @@ Arguments mmap {A B _} f !s /.
+ Class MMapExt (A B : Type) `{MMap A B} := 
+   mmap_ext : forall f g,
+     (forall t, f t = g t) -> forall s, mmap f s = mmap g s.
+-Arguments mmap_ext {A B _ _ f g} H s.
++Arguments mmap_ext {A B H' _ f g} H s : rename.
+
+ Class MMapLemmas (A B : Type) `{MMap A B} := {
+   mmap_id x : mmap id x = x;
+@@ -123,6 +123,7 @@ Tactic Notation "msimpl" "in" "*" := (in_all msimplH); msimpl.
+
+ Ltac derive_MMap :=
+   hnf; match goal with [ |- (?A -> ?A) -> ?B -> ?B ] =>
++    let map := fresh "map" in
+     intros f; fix map 1; intros xs; change (annot B xs); destruct xs;
+     match goal with
+       | [ |- annot _ ?ys ] =>
+-- 
+2.13.2
+
diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix
@@ -0,0 +1,27 @@
+{ stdenv, fetchgit, coq, mathcomp }:
+
+stdenv.mkDerivation rec {
+
+  name = "coq-autosubst-${coq.coq-version}-${version}";
+  version = "5b40a32e";
+
+  src = fetchgit {
+    url = git://github.com/uds-psl/autosubst.git;
+    rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034";
+    sha256 = "1wqfzc9az85fvx71xxfii502jgc3mp0r3xwfb8vnb03vkk625ln0";
+  };
+
+  propagatedBuildInputs = [ mathcomp ];
+
+  patches = [./0001-changes-to-work-with-Coq-8.6.patch];
+
+  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  meta = with stdenv.lib; {
+    homepage = https://www.ps.uni-saarland.de/autosubst/;
+    description = "Automation for de Bruijn syntax and substitution in Coq";
+    maintainers = with maintainers; [ jwiegley ];
+    platforms = coq.meta.platforms;
+  };
+
+}
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix
@@ -3,11 +3,11 @@
 stdenv.mkDerivation rec {
 
   name = "coq-paco-${coq.coq-version}-${version}";
-  version = "1.2.7";
+  version = "1.2.8";
 
   src = fetchurl {
     url = "http://plv.mpi-sws.org/paco/paco-${version}.zip";
-    sha256 = "010fs74c0cmb9sz5dmrgzg4pmb2mgwia4gm0g9l7j2fq5xxcschb";
+    sha256 = "1lcmdr0y2d7gzyvr8dal3pi7fibbd60bpi1l32fw89xiyrgqhsqy";
   };
 
   buildInputs = [ coq.ocaml coq.camlp5 unzip ];

diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
@@ -18013,6 +18013,7 @@ with pkgs;
     };
     coqPackages = coqPackages_8_5;
 
+    autosubst = callPackage ../development/coq-modules/autosubst {};
     coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
     coquelicot = callPackage ../development/coq-modules/coquelicot {};
     dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
@@ -18031,10 +18032,12 @@ with pkgs;
     coq = callPackage ../applications/science/logic/coq {};
     coqPackages = coqPackages_8_6;
 
+    autosubst = callPackage ../development/coq-modules/autosubst {};
     coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
     coquelicot = callPackage ../development/coq-modules/coquelicot {};
     dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
     flocq = callPackage ../development/coq-modules/flocq {};
+    heq = callPackage ../development/coq-modules/heq {};
     interval = callPackage ../development/coq-modules/interval {};
     mathcomp = callPackage ../development/coq-modules/mathcomp { };
     paco = callPackage ../development/coq-modules/paco {};