aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Modularisation des preuves concernant la logique classique, ↵Gravatar herbelin2006-03-05
| | | | | | l'indiscernabilité des preuves et l'axiome K git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8136 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar herbelin2006-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage du IP classique pour éviter confusion avec IP constructifGravatar herbelin2006-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout étude IP généralisé, Gödel-Dummett, buveurGravatar herbelin2006-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite simplification en passantGravatar herbelin2006-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8122 85f007b7-540e-0410-9357-904b9bb8a0f7
* Titres moins envahissants pour coqdocGravatar herbelin2006-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8121 85f007b7-540e-0410-9357-904b9bb8a0f7
* quelques raccourcis commodes + un f_equal plus efficaceGravatar letouzey2006-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'exists! x:A, P (suite)Gravatar herbelin2006-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8086 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'exists! x:A, PGravatar herbelin2006-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minimum pour documentation TeX de la biblioGravatar herbelin2006-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8082 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug ScopeGravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage Zmin.v, création Zmax.v et Zminmax.vGravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage Bool:Gravatar herbelin2006-02-12
| | | | | | | | | | | | | | | | 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
* Unification max_case et max_case2Gravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification min_case et min_case2Gravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commentaires et compatibilité coqdocGravatar herbelin2006-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8026 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2006-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bibliothèque String de Laurent ThéryGravatar herbelin2006-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8009 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et ↵Gravatar herbelin2006-02-06
| | | | | | Russell O'Connor (redondance Acc_iter et Fix_F) + uniformisation indentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout décidabilitéGravatar herbelin2006-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7965 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application de la suggestion de Nicolas Magaud (#1060)Gravatar herbelin2006-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind ↵Gravatar herbelin2006-01-21
| | | | | | est incompatible avec la préservation du type de Acc_intro (par uniformité de notations, x est finalement préféré) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7912 85f007b7-540e-0410-9357-904b9bb8a0f7
* Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de AccGravatar herbelin2006-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7905 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction associativité de IF et exists (visible à l'affichage uniquement ↵Gravatar herbelin2006-01-19
| | | | | | à cause du traitement spécial du niveau binder_constr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application du souhait de transparence de well_founded_ltof (#1007)Gravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contrepartie de la suppression des boites automatiques dans formatGravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7703 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement parametres inductifs dans les theoriesGravatar mohring2005-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7630 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar letouzey2005-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7322 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix sumbool_not hint (on behalf of cpaulin).Gravatar coq2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7235 85f007b7-540e-0410-9357-904b9bb8a0f7
* add a left and right tactic for classical logicGravatar narboux2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7234 85f007b7-540e-0410-9357-904b9bb8a0f7
* Détection d'un Fold incorrect suite à correction bug #986Gravatar herbelin2005-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7
* Détection d'un Fold incorrect suite à correction bug #986Gravatar herbelin2005-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7219 85f007b7-540e-0410-9357-904b9bb8a0f7
* DocumentationGravatar herbelin2005-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement, préservation de la compatibilité pour Z_lt_induction et ajout ↵Gravatar herbelin2005-05-02
| | | | | | plutôt de nouveaux énoncés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lemme de passage de l'autre côté d'une égalitéGravatar herbelin2005-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed hypotheses of Z_lt_induction (see #957)Gravatar herbelin2005-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added option_mapGravatar herbelin2005-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Missing translating a 'O' into a '0' (again - cf bug #947); removed useless ↵Gravatar herbelin2005-03-29
| | | | | | hypothesis of Zlt/Zgt_square_simpl (cg #948) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6898 85f007b7-540e-0410-9357-904b9bb8a0f7
* Missing translating a 'O' into a '0' (again)Gravatar herbelin2005-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Missing translating a 'O' into a '0'Gravatar herbelin2005-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6884 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ PolyList -> ListGravatar herbelin2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6844 85f007b7-540e-0410-9357-904b9bb8a0f7
* quelques tactics ltacGravatar letouzey2005-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6773 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des ↵Gravatar coq2005-02-07
| | | | | | jours de calcul (chapitre 16, thm prime_2333); peut-être à cause de Z_of_nat??) [HH] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'Unboxed des opérations sur positive (cf bug 898)Gravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai d'utilisation de 'where' pour les notationsGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursGravatar herbelin2005-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6670 85f007b7-540e-0410-9357-904b9bb8a0f7
* legere simplification des preuves de le_S_n et pred_leGravatar letouzey2005-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursGravatar herbelin2005-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6666 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-29 00:52:08 +0000