From 86803d3a98dc95bc8935da9ad9ef0703c621a533 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Sat, 13 Feb 2016 11:54:15 +0100
Subject: [PATCH] Make reflexivity hints work for evars.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Since Coq 8.4 did not backtrack on eauto premises, we used to ensure
that hints like
Hint Extern 0 (?x ≡{_}≡ ?y) => reflexivity.
were not used for goals involving evars by writing ?x ≡{_}≡ ?y instead
of _ ≡{_}≡ _.
This seems to be a legacy issue that no longer applies to Coq 8.5, so
I have removed these restrictions making these hints thus more powerful.
---
theories/base.v | 4 ++--
theories/list.v | 8 ++++----
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index 3f30a11..f711649 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -53,7 +53,7 @@ Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : C_scope.
Notation "( x ≠)" := (λ y, x ≠ y) (only parsing) : C_scope.
Notation "(≠ x )" := (λ y, y ≠ x) (only parsing) : C_scope.
-Hint Extern 0 (?x = ?x) => reflexivity.
+Hint Extern 0 (_ = _) => reflexivity.
Hint Extern 100 (_ ≠ _) => discriminate.
Notation "(→)" := (λ A B, A → B) (only parsing) : C_scope.
@@ -198,7 +198,7 @@ Instance: Params (@equiv) 2.
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3.
-Hint Extern 0 (?x ≡ ?y) => reflexivity.
+Hint Extern 0 (_ ≡ _) => reflexivity.
Hint Extern 0 (_ ≡ _) => symmetry; assumption.
(** ** Operations on collections *)
diff --git a/theories/list.v b/theories/list.v
index d0e0eaf..34645ee 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -220,8 +220,8 @@ Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
Definition prefix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.
-Hint Extern 0 (?x `prefix_of` ?y) => reflexivity.
-Hint Extern 0 (?x `suffix_of` ?y) => reflexivity.
+Hint Extern 0 (_ `prefix_of` _) => reflexivity.
+Hint Extern 0 (_ `suffix_of` _) => reflexivity.
Section prefix_suffix_ops.
Context `{∀ x y : A, Decision (x = y)}.
@@ -249,7 +249,7 @@ Inductive sublist {A} : relation (list A) :=
| sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
| sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
Infix "`sublist`" := sublist (at level 70) : C_scope.
-Hint Extern 0 (?x `sublist` ?y) => reflexivity.
+Hint Extern 0 (_ `sublist` _) => reflexivity.
(** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
from [l1] while possiblity changing the order. *)
@@ -260,7 +260,7 @@ Inductive contains {A} : relation (list A) :=
| contains_cons x l1 l2 : contains l1 l2 → contains l1 (x :: l2)
| contains_trans l1 l2 l3 : contains l1 l2 → contains l2 l3 → contains l1 l3.
Infix "`contains`" := contains (at level 70) : C_scope.
-Hint Extern 0 (?x `contains` ?y) => reflexivity.
+Hint Extern 0 (_ `contains` _) => reflexivity.
Section contains_dec_help.
Context {A} {dec : ∀ x y : A, Decision (x = y)}.
--
2.24.1