Commit b144f52f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent 599d7411
......@@ -122,7 +122,6 @@ Qed.
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
{ uPred_in_entails : n x, {n} x P n x Q n x }.
Hint Extern 0 (uPred_entails _ _) => reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Hint Resolve uPred_mono uPred_closed : uPred_def.
......@@ -13,6 +13,12 @@ Export ListNotations.
From Coq.Program Require Export Basics Syntax.
Obligation Tactic := idtac.
Instance default_rewrite_relation {A} (R : relation A) : RewriteRelation R.
Remove Hints RewriteRelation_instance_0
RewriteRelation_instance_1 RewriteRelation_instance_2
equivalence_rewrite_relation : typeclass_instances.
(** Throughout this development we use [C_scope] for all general purpose
notations that do not belong to a more specific scope. *)
Delimit Scope C_scope with C.
Markdown is supported
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