Commit 51d69170 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

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.
parent a99446f9
......@@ -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.
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).
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment