Commit af27fc8a authored by Dan Frumin's avatar Dan Frumin

Use more `!`s in the Hint Modes.

parent 8298b612
......@@ -22,7 +22,7 @@ which are supposed to be treated as output. *)
(** ** IntoDBool *)
Class IntoDBool (b : bool) (db : dbool) :=
into_dbool : b = dbool_interp db.
Hint Mode IntoDBool + - : typeclass_instances.
Hint Mode IntoDBool ! - : typeclass_instances.
Instance into_dbool_true : IntoDBool true (dBoolKnown true).
Proof. done. Qed.
......@@ -34,7 +34,7 @@ Proof. done. Qed.
(** ** IntoDInt *)
Class NatIntoDInt (n : nat) (di : dint) :=
nat_into_dint : Z.of_nat n = dint_interp di.
Hint Mode NatIntoDInt + - : typeclass_instances.
Hint Mode NatIntoDInt ! - : typeclass_instances.
Instance nat_into_dint_0 : NatIntoDInt 0 (dInt 0 None).
Proof. done. Qed.
......@@ -50,7 +50,7 @@ Proof. done. Qed.
Class ZIntoDInt (i : Z) (di : dint) :=
Z_into_dint : i = dint_interp di.
Hint Mode ZIntoDInt + - : typeclass_instances.
Hint Mode ZIntoDInt ! - : typeclass_instances.
Instance Z_into_dint_nat n di : NatIntoDInt n di ZIntoDInt (Z.of_nat n) di | 0.
Proof. done. Qed.
......@@ -75,7 +75,7 @@ Class LocLookup (E E' : known_locs) (cl : cloc) (i : nat) := {
loc_lookup : E' !! i = Some cl;
loc_lookup_mono : E `prefix_of` E';
}.
Hint Mode LocLookup + - + - : typeclass_instances.
Hint Mode LocLookup ! - ! - : typeclass_instances.
Instance loc_lookup_new cl : LocLookup [] [cl] cl 0.
Proof. split. done. by exists [cl]. Qed.
......@@ -91,7 +91,7 @@ Class IntoDLoc (E E' : known_locs) (cl : cloc) (dl : dloc) := {
into_dloc_wf : dloc_wf E' dl;
into_dloc_mono : E `prefix_of` E';
}.
Hint Mode IntoDLoc + - + - : typeclass_instances.
Hint Mode IntoDLoc ! - ! - : typeclass_instances.
Instance into_dloc_lookup E E' cl i :
LocLookup E E' cl i IntoDLoc E E' cl (dLoc i (dInt 0 None)) | 10.
......@@ -112,7 +112,7 @@ Qed.
(** ** IntoDBaseLit *)
Class IntoDBaseLit (l : base_lit) (dl : dbase_lit) :=
into_dbase_lit : l = dbase_lit_interp dl.
Hint Mode IntoDBaseLit + - : typeclass_instances.
Hint Mode IntoDBaseLit ! - : typeclass_instances.
Instance into_dbase_lit_int i di :
ZIntoDInt i di IntoDBaseLit (LitInt i) (dLitInt di).
......@@ -131,7 +131,7 @@ Class IntoDVal (E E' : known_locs) (v : val) (dv : dval) := {
into_dval_wf : dval_wf E' dv;
into_dval_mono : E `prefix_of` E';
}.
Hint Mode IntoDVal + - + - : typeclass_instances.
Hint Mode IntoDVal ! - ! - : typeclass_instances.
Instance into_dval_base_lit E l dl :
IntoDBaseLit l dl IntoDVal E E (LitV l) (dLitV dl).
......@@ -158,7 +158,7 @@ Class IntoDExpr (E E' : known_locs) (e: expr) (de: dexpr) := {
into_dexpr_wf : dexpr_wf E' de;
into_dexpr_mono : E `prefix_of` E';
}.
Hint Mode IntoDExpr + - + - : typeclass_instances.
Hint Mode IntoDExpr ! - ! - : typeclass_instances.
Instance into_dexpr_val E E' v dv :
IntoDVal E E' v dv IntoDExpr E E' (Val v) (dEVal dv).
......@@ -190,7 +190,7 @@ Class IntoDCExpr (E E' : known_locs) (e: expr) (de: dcexpr) := {
into_dcexpr_wf : dcexpr_wf E' de;
into_dcexpr_mono : E `prefix_of` E';
}.
Hint Mode IntoDCExpr + - + - : typeclass_instances.
Hint Mode IntoDCExpr ! - ! - : typeclass_instances.
Local Ltac solve_into_dcexpr2 :=
intros [-> ??] [-> ??]; split=> /=;
......
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