@@ -1,134 +0,0 @@
1−From 5b40a32e35fe446cda20ed34c756a010856f39ce Mon Sep 17 00:00:00 2001
2−From: Theo Giannakopoulos <theo.giannakopoulos@baesystems.com>
3−Date: Wed, 5 Apr 2017 15:48:55 -0400
4−Subject: [PATCH] changes to work with Coq 8.6
5−
6−---
7− theories/Autosubst_Derive.v | 12 ++++++++++++
8− theories/Autosubst_MMap.v | 3 ++-
9− 2 files changed, 14 insertions(+), 1 deletion(-)
10−
11−diff --git a/theories/Autosubst_Derive.v b/theories/Autosubst_Derive.v
12−index 61995de..cf87f67 100644
13−--- a/theories/Autosubst_Derive.v
14−+++ b/theories/Autosubst_Derive.v
15−@@ -18,6 +18,7 @@ Hint Extern 0 (Ids _) => derive_Ids : derive.
16−
17− Ltac derive_Rename :=
18− match goal with [ |- Rename ?term ] =>
19−+ let inst := fresh "inst" in
20− hnf; fix inst 2; change _ with (Rename term) in inst;
21− intros xi s; change (annot term s); destruct s;
22− match goal with
23−@@ -66,6 +67,7 @@ Ltac has_var s :=
24− Ltac derive_Subst :=
25− match goal with [ |- Subst ?term ] =>
26− require_instance (Rename term);
27−+ let inst := fresh "inst" in
28− hnf; fix inst 2; change _ with (Subst term) in inst;
29− intros sigma s; change (annot term s); destruct s;
30− match goal with
31−@@ -107,6 +109,7 @@ Hint Extern 0 (Subst _) => derive_Subst : derive.
32− Ltac derive_HSubst :=
33− match goal with [ |- HSubst ?inner ?outer ] =>
34− require_instance (Subst inner);
35−+ let inst := fresh "inst" in
36− hnf; fix inst 2; change _ with (HSubst inner outer) in inst;
37− intros sigma s; change (annot outer s); destruct s;
38− match goal with
39−@@ -327,6 +330,7 @@ Ltac derive_SubstLemmas :=
40− assert (up_upren_n :
41− forall xi n, upn n (ren xi) = ren (iterate upren n xi)) by
42− (apply up_upren_n_internal, up_upren);
43−+ let ih := fresh "ih" in
44− fix ih 2; intros xi s; destruct s; try reflexivity; simpl; f_equal;
45− try apply mmap_ext; intros; rewrite ?up_upren, ?up_upren_n; apply ih);
46−
47−@@ -337,6 +341,7 @@ Ltac derive_SubstLemmas :=
48− (apply up_id_internal; reflexivity);
49− assert (up_id_n : forall n, upn n ids = ids) by
50− (apply up_id_n_internal, up_id);
51−+ let ih := fresh "ih" in
52− fix ih 1; intros s; destruct s; simpl; f_equal; try reflexivity;
53− rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; apply ih);
54−
55−@@ -344,6 +349,7 @@ Ltac derive_SubstLemmas :=
56−
57− assert (ren_subst_comp :
58− forall xi sigma (s : term), (rename xi s).[sigma] = s.[xi >>> sigma]) by(
59−+ let ih := fresh "ih" in
60− fix ih 3; intros xi sigma s; destruct s; try reflexivity; simpl; f_equal;
61− rewrite ?up_comp_ren_subst, ?up_comp_ren_subst_n, ?mmap_comp;
62− try apply mmap_ext; intros; apply ih);
63−@@ -357,6 +363,7 @@ Ltac derive_SubstLemmas :=
64− assert (up_comp_subst_ren_n :
65− forall sigma xi n, upn n (sigma >>> rename xi) = upn n sigma >>> rename (iterate upren n xi))
66− by (apply up_comp_subst_ren_n_internal; apply up_comp_subst_ren);
67−+ let ih := fresh "ih" in
68− fix ih 3; intros sigma xi s; destruct s; try reflexivity; simpl;
69− f_equal; rewrite ?up_comp_subst_ren, ?up_comp_subst_ren_n, ?mmap_comp;
70− try (rewrite hcomp_ren_internal; [|apply rename_subst]);
71−@@ -368,6 +375,7 @@ Ltac derive_SubstLemmas :=
72− by (apply up_comp_internal; [reflexivity|apply ren_subst_comp|apply subst_ren_comp]);
73− assert (up_comp_n : forall sigma tau n, upn n (sigma >> tau) = upn n sigma >> upn n tau)
74− by (apply up_comp_n_internal; apply up_comp);
75−+ let ih := fresh "ih" in
76− fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal;
77− rewrite ?up_comp, ?up_comp_n, ?mmap_comp, ?hcomp_dist_internal;
78− try apply mmap_ext; intros; apply ih);
79−@@ -382,6 +390,7 @@ Ltac derive_HSubstLemmas :=
80− let ids := constr:(ids : var -> inner) in
81−
82− assert (hsubst_id : forall (s : outer), s.|[ids] = s) by (
83−+ let ih := fresh "ih" in
84− fix ih 1; intros s; destruct s; try reflexivity; simpl; f_equal;
85− rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros;
86− (apply subst_id || apply ih)
87−@@ -390,6 +399,7 @@ Ltac derive_HSubstLemmas :=
88− assert (hsubst_comp : forall (theta eta : var -> inner) (s : outer),
89− s.|[theta].|[eta] = s.|[theta >> eta])
90− by (
91−+ let ih := fresh "ih" in
92− fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal;
93− rewrite <- ?up_comp, <- ?up_comp_n, ?mmap_comp; try apply mmap_ext; intros;
94− (apply subst_comp || apply ih)
95−@@ -405,6 +415,7 @@ Ltac derive_SubstHSubstComp :=
96− assert (ren_hsubst_comp : forall xi (theta : var -> inner) (s : outer),
97− rename xi s.|[theta] = (rename xi s).|[theta]
98− ) by (
99−+ let ih := fresh "ih" in
100− fix ih 3; intros xi theta s; destruct s; try reflexivity; simpl; f_equal;
101− rewrite ?mmap_comp; try apply mmap_ext; intros; simpl; apply ih
102− );
103−@@ -421,6 +432,7 @@ Ltac derive_SubstHSubstComp :=
104− apply up_hcomp_n_internal; apply up_hcomp
105− );
106−
107−+ let ih := fresh "ih" in
108− fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal;
109− rewrite ?up_hcomp, ?up_hcomp_n, ?hcomp_lift_n_internal, ?mmap_comp;
110− try apply mmap_ext; intros; apply ih
111−diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
112−index f8387e7..7af7902 100644
113−--- a/theories/Autosubst_MMap.v
114−+++ b/theories/Autosubst_MMap.v
115−@@ -23,7 +23,7 @@ Arguments mmap {A B _} f !s /.
116− Class MMapExt (A B : Type) `{MMap A B} :=
117− mmap_ext : forall f g,
118− (forall t, f t = g t) -> forall s, mmap f s = mmap g s.
119−-Arguments mmap_ext {A B _ _ f g} H s.
120−+Arguments mmap_ext {A B H' _ f g} H s : rename.
121−
122− Class MMapLemmas (A B : Type) `{MMap A B} := {
123− mmap_id x : mmap id x = x;
124−@@ -123,6 +123,7 @@ Tactic Notation "msimpl" "in" "*" := (in_all msimplH); msimpl.
125−
126− Ltac derive_MMap :=
127− hnf; match goal with [ |- (?A -> ?A) -> ?B -> ?B ] =>
128−+ let map := fresh "map" in
129− intros f; fix map 1; intros xs; change (annot B xs); destruct xs;
130− match goal with
131− | [ |- annot _ ?ys ] =>
132−--
133−2.13.2
134−