From 8d0efe8e84f9e23e8361f9948288d69d9b90b3df Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Sat, 28 Oct 2017 15:25:39 +0200
Subject: [PATCH] remove Set Asymmetric Patterns
---
theories/base.v | 1 -
theories/fin.v | 4 ++--
theories/finite.v | 2 +-
theories/hlist.v | 8 ++++----
theories/option.v | 2 +-
theories/vector.v | 2 +-
6 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index f0964e3..56dcd6a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -5,7 +5,6 @@ that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, collections, and various other data
structures. *)
Global Generalizable All Variables.
-Global Set Asymmetric Patterns.
Global Unset Transparent Obligations.
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
Set Default Proof Using "Type".
diff --git a/theories/fin.v b/theories/fin.v
index 4b8cdd0..6dc71b1 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -28,7 +28,7 @@ Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope.
Notation "10" := (FS 9) : fin_scope.
Fixpoint fin_to_nat {n} (i : fin n) : nat :=
- match i with 0%fin => 0 | FS _ i => S (fin_to_nat i) end.
+ match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.
Coercion fin_to_nat : fin >-> nat.
Notation fin_of_nat := Fin.of_nat_lt.
@@ -57,7 +57,7 @@ Definition fin_S_inv {n} (P : fin (S n) → Type)
(H0 : P 0%fin) (HS : ∀ i, P (FS i)) (i : fin (S n)) : P i.
Proof.
revert P H0 HS.
- refine match i with 0%fin => λ _ H0 _, H0 | FS _ i => λ _ _ HS, HS i end.
+ refine match i with 0%fin => λ _ H0 _, H0 | FS i => λ _ _ HS, HS i end.
Defined.
Ltac inv_fin i :=
diff --git a/theories/finite.v b/theories/finite.v
index aba0ae9..ab14c0e 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -72,7 +72,7 @@ Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
Fin.of_nat_lt (encode_lt_card x).
Program Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
match Some_dec (decode_nat i) return _ with
- | inleft (exist x _) => x | inright _ => _
+ | inleft (exist _ x _) => x | inright _ => _
end.
Next Obligation.
intros A ?? i ?; exfalso.
diff --git a/theories/hlist.v b/theories/hlist.v
index 90a9830..ae4f934 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -14,12 +14,12 @@ Inductive hlist : tlist → Type :=
Fixpoint tapp (As Bs : tlist) : tlist :=
match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
- match xs with hnil => ys | hcons _ _ x xs => hcons x (happ xs ys) end.
+ match xs with hnil => ys | hcons x xs => hcons x (happ xs ys) end.
Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
- match xs with hnil => () | hcons _ _ x _ => x end.
+ match xs with hnil => () | hcons x _ => x end.
Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
- match xs with hnil => () | hcons _ _ _ xs => xs end.
+ match xs with hnil => () | hcons _ xs => xs end.
Fixpoint hheads {As Bs} : hlist (tapp As Bs) → hlist As :=
match As with
@@ -43,7 +43,7 @@ Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
(fix go As xs :=
match xs in hlist As return himpl As B → B with
| hnil => λ f, f
- | hcons A As x xs => λ f, go As xs (f x)
+ | @hcons A As x xs => λ f, go As xs (f x)
end) _ xs f.
Coercion hcurry : himpl >-> Funclass.
diff --git a/theories/option.v b/theories/option.v
index 9f5b7ef..d50cc7e 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -65,7 +65,7 @@ Proof.
set (f mx := match mx return P mx → is_Some mx with
Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
set (g mx (H : is_Some mx) :=
- match H return P mx with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end).
+ match H return P mx with ex_intro _ _ p => eq_rect _ _ I _ (eq_sym p) end).
assert (∀ mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst).
intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
Qed.
diff --git a/theories/vector.v b/theories/vector.v
index 69b31fe..e46774e 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -238,7 +238,7 @@ Qed.
Fixpoint vinsert {A n} (i : fin n) (x : A) : vec A n → vec A n :=
match i with
| 0%fin => vec_S_inv _ (λ _ v, x ::: v)
- | FS _ i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
+ | FS i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
end.
Lemma vec_to_list_insert {A n} i x (v : vec A n) :
--
GitLab