diff --git a/prelude/base.v b/prelude/base.v index 8f01258a121363b1fab7f29949b8ae6957fb2800..c097a713a84be653b8378b01fc677331f7c49d2d 100644 --- a/prelude/base.v +++ b/prelude/base.v @@ -375,8 +375,6 @@ Notation zip := (zip_with pair). Coercion Is_true : bool >-> Sortclass. Hint Unfold Is_true. Hint Immediate Is_true_eq_left. -Existing Class Is_true. -Instance true_Is_true : Is_true true := I. Hint Resolve orb_prop_intro andb_prop_intro. Notation "(&&)" := andb (only parsing). Notation "(||)" := orb (only parsing).