coqPackages.autosubst: 5b40a32e -> 1.7 and fix build

2 files changed, 13 insertions, 146 deletions

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
deleted file mode 100644
index dde0e2e03eb6..000000000000
--- a/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch
+++ /dev/null
@@ -1,134 +0,0 @@
-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
index b2609d5dfc32..a5f7cbb2f0b1 100644
--- a/pkgs/development/coq-modules/autosubst/default.nix
+++ b/pkgs/development/coq-modules/autosubst/default.nix
@@ -1,22 +1,23 @@
-{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
+{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }:
+with lib;
 
-with lib; mkCoqDerivation {
-  pname   = "autosubst";
-  owner   = "uds-psl";
-  inherit version;
-  defaultVersion = with versions;
-    if range "8.5" "8.7" coq.coq-version then "5b40a32e" else null;
+mkCoqDerivation {
+  pname = "autosubst";
 
-  release."5b40a32e".rev    = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034";
-  release."5b40a32e".sha256 = "1wqfzc9az85fvx71xxfii502jgc3mp0r3xwfb8vnb03vkk625ln0";
+  release."1.7".rev    = "v1.7";
+  release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI=";
 
-  propagatedBuildInputs = [ mathcomp.ssreflect ];
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.10"; out = "1.7"; }
+  ] null;
 
-  patches = [./0001-changes-to-work-with-Coq-8.6.patch];
+  propagatedBuildInputs = [ mathcomp-ssreflect ];
 
   meta = {
     homepage = "https://www.ps.uni-saarland.de/autosubst/";
     description = "Automation for de Bruijn syntax and substitution in Coq";
-    maintainers = with maintainers; [ jwiegley ];
+    maintainers = with maintainers; [ siraben jwiegley ];
+    license = licenses.mit;
   };
 }