From 51d691702e7494c93a4cdc5d899ba2e5ebbb4a2d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Jan 2019 18:28:26 +0100
Subject: [PATCH] Remove `ars` hint database.
The name made no sense and it was not used anywhere to my knowledge. If it
was used anywhere, it would be very unreliable as it contained hints like
`rtc_trans` that would generally lead to loops.
---
theories/relations.v | 7 +------
1 file changed, 1 insertion(+), 6 deletions(-)
diff --git a/theories/relations.v b/theories/relations.v
index 0811a9b6..51644dac 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -2,8 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on abstract rewriting systems.
These are particularly useful as we define the operational semantics as a
-small step semantics. This file defines a hint database [ars] containing
-some theorems on abstract rewriting systems. *)
+small step semantics. *)
From Coq Require Import Wf_nat.
From stdpp Require Export tactics base.
Set Default Proof Using "Type".
@@ -190,10 +189,6 @@ Section rtc.
Qed.
End rtc.
-Hint Constructors rtc nsteps bsteps tc : ars.
-Hint Resolve rtc_once rtc_r tc_r rtc_transitive tc_rtc_l tc_rtc_r
- tc_rtc bsteps_once bsteps_r bsteps_refl bsteps_trans : ars.
-
(** * Theorems on sub relations *)
Section subrel.
Context {A} (R1 R2 : relation A).
--
GitLab