diff options
Diffstat (limited to 'pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch')
| -rw-r--r-- | pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch | 134 |
1 files changed, 0 insertions, 134 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 dde0e2e03eb..00000000000 --- 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 - |