Skip to content
Snippets Groups Projects
Commit dad9e782 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix `Arguments` of `ElimInv`. 

Thanks to @jtassaro for reporting.
parent 6bca8573
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/classes.v
+ 2
− 2
View file @ dad9e782
...@@ -501,8 +501,8 @@ Hint Mode IntoInv + ! - : typeclass_instances. ...@@ -501,8 +501,8 @@ Hint Mode IntoInv + ! - : typeclass_instances.
*) *)
Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) := Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ Pclose -∗ Q') ⊢ Q. elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ Pclose -∗ Q') ⊢ Q.
Arguments ElimInv {_} _ _ _%I _%I _%I _%I : simpl never. Arguments ElimInv {_} _ _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} _ _ _%I _%I _%I _%I _%I _%I. Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I _%I.
Hint Mode ElimInv + - ! - - - ! - : typeclass_instances. Hint Mode ElimInv + - ! - - - ! - : typeclass_instances.
(* We make sure that tactics that perform actions on *specific* hypotheses or (* We make sure that tactics that perform actions on *specific* hypotheses or
......
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