diff options
Diffstat (limited to 'nixpkgs/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch')
| -rw-r--r-- | nixpkgs/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch | 134 |
1 files changed, 134 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch b/nixpkgs/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch new file mode 100644 index 00000000000..dde0e2e03eb --- /dev/null +++ b/nixpkgs/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 + |