Commit 8298b612 authored by Dan Frumin's avatar Dan Frumin

Better Hint Modes.

parent eddaf56d
......@@ -15,7 +15,7 @@ Class IntoDEnv `{cmonadG Σ} (E E' : known_locs) (Γin Γout : env (iProp Σ)) (
into_denv_mono : E `prefix_of` E';
}.
Arguments IntoDEnv {_ _} _ _ _ _ _.
Hint Mode IntoDEnv - - + - + - - : typeclass_instances.
Hint Mode IntoDEnv - - ! - + - - : typeclass_instances.
(** Given a proposition [Pin] and a symbolic heap [m] potentially adds
[Pin] to the symbolic heap (resulting in [m2]), replacing [Pin] with
......@@ -29,8 +29,8 @@ Class PropIntoDEnv `{cmonadG Σ} (E E' : known_locs) (Pin Pout : iProp Σ) (m1 m
prop_into_denv_wf : denv_wf E m1 denv_wf E' m2;
prop_into_denv_mono : E `prefix_of` E';
}.
Arguments PropIntoDEnv {_ _} _ _ _%I _%I _.
Hint Mode PropIntoDEnv - - + - + - + - : typeclass_instances.
Arguments PropIntoDEnv {_ _} _ _ _%I _%I _ _.
Hint Mode PropIntoDEnv - - + - ! - + - : typeclass_instances.
Section tactics.
Context `{cmonadG Σ}.
......
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