diff options
| author | herbelin | 2006-02-12 19:22:31 +0000 |
|---|---|---|
| committer | herbelin | 2006-02-12 19:22:31 +0000 |
| commit | aff35869e7010a13e9ac02358804be49e26c4d83 (patch) | |
| tree | 5a7f63894ff860f1bc5dcb0778f6b4e1b31cca52 /kernel/type_errors.mli | |
| parent | 508603af923a1c0430b19c3cc28720a50ee90667 (diff) | |
Nettoyage Bool:
Suppression de bool_2, bool_4 et bool_5 très ad hoc
Renommage des lemmes demorgan* qui n'énoncent en fait pas les lois de de Morgan
Tentative partielle de renommage (un peu) plus uniforme
Pour les Hint:
- bool_5 de core remplacé en mettant exact diff_false_true dans core (un
peu plus faible mais marche dans la pratique pour les contribs)
- bool_2 remplacé par la transitivité sur bool (plus fort mais OK dans la
pratique, et pas trop fort pour ne pas atteindre la force de trans_eq)
- bool_4 apparemment pas utilisé
- andb_false_elim, spécifique, apparemment pas utilisé, et supprimé comme hint
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8031 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions