Skip to content
Snippets Groups Projects

Set the priority of the rewrite relation for sqsubseteq to not take precedence over...

Merged Set the priority of the rewrite relation for sqsubseteq to not take precedence over...
mattam82/stdpp:pr-13969-take3 into master
All threads resolved!
Merged Matthieu Sozeau requested to merge mattam82/stdpp:pr-13969-take3 into master
All threads resolved!
Compare
and
1 file
+ 2
− 1
Compare changes
  • Side-by-side
  • Inline
theories/base.v
+ 2
− 1
@@ -1359,7 +1359,8 @@ Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
@@ -1359,7 +1359,8 @@ Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
+1
(** [sqsubseteq] does not take precedence over the stdlib's instances or [equiv]. *)
 
Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 200 := {}.
Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.