Skip to content
Snippets Groups Projects
Commit d927b406 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix Hint Mode.

parent 7c714af0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/monpred.v
+ 1
− 1
View file @ d927b406
...@@ -6,7 +6,7 @@ Class MakeMonPredCar {I : bi_index} {PROP : bi} (i : I) ...@@ -6,7 +6,7 @@ Class MakeMonPredCar {I : bi_index} {PROP : bi} (i : I)
(P : monPred I PROP) (𝓟 : PROP) := (P : monPred I PROP) (𝓟 : PROP) :=
make_monPred_car : P i ⊣⊢ 𝓟. make_monPred_car : P i ⊣⊢ 𝓟.
Arguments MakeMonPredCar {_ _} _ _%I _%I. Arguments MakeMonPredCar {_ _} _ _%I _%I.
Hint Mode MakeMonPredCar + + - ! -. Hint Mode MakeMonPredCar + + - ! - : typeclass_instances.
Section bi. Section bi.
Context {I : bi_index} {PROP : bi}. Context {I : bi_index} {PROP : bi}.
......
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