Skip to content
Snippets Groups Projects
Commit 36bc5009 authored by Matthieu Sozeau's avatar Matthieu Sozeau
Browse files

Fix sqsubseteq_rewrite's priority, making it lower than equiv

parent 607ee2b1
No related branches found
No related tags found
No related merge requests found
...@@ -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}) := {}. (** [sqsubseteq] does not take precedence over the stdlib's instances or [equiv]. *)
Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 160 := {}.
Global Hint Extern 0 (_ _) => reflexivity : core. Global Hint Extern 0 (_ _) => reflexivity : core.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment