dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

Removed bad hints

This commit is contained in:
Niels 2017-08-01 17:35:23 +02:00
parent e6bf0f9d5d
commit 5ee7053631
2 changed files with 5 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
FiniteSets/disjunction.v
View File

@ -84,7 +84,7 @@ Open Scope logic_scope.
Section hPropLattice. Section hPropLattice.
Context `{Univalence}. Context `{Univalence}.
Instance lor_commutative : Commutative lor. Global Instance lor_commutative : Commutative lor.
Proof. Proof.
unfold Commutative. unfold Commutative.
intros. intros.
@ -183,10 +183,3 @@ Section hPropLattice.
}. }.
End hPropLattice. End hPropLattice.
Hint Resolve
commutative_min commutative_max associative_min associative_max
idempotent_min idempotent_max
neutralL_min neutralR_min
absorption_min_max absorption_max_min
: lattice_hints.

6
FiniteSets/fsets/operations.v
View File

@ -17,9 +17,9 @@ hrecursion.
exact _. exact _.
- apply lor. - apply lor.
- intros ; symmetry ; apply lor_assoc. - intros ; symmetry ; apply lor_assoc.
- intros ; apply lor_comm. - apply lor_commutative.
- intros ; apply lor_nl. - apply lor_nl.
- intros ; apply lor_nr. - apply lor_nr.
- intros ; apply lor_idem. - intros ; apply lor_idem.
Defined. Defined.