aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8009 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et ↵herbelin
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
2006-01-31Ajout décidabilitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7965 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-22Application de la suggestion de Nicolas Magaud (#1060)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7917 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind ↵herbelin
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
2006-01-21Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Accherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7905 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Correction associativité de IF et exists (visible à l'affichage uniquement ↵herbelin
à 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
2005-12-30Application du souhait de transparence de well_founded_ltof (#1007)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7766 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22Contrepartie de la suppression des boites automatiques dans formatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7703 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-30changement parametres inductifs dans les theoriesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7630 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-26*** empty log message ***letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7322 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15Fix sumbool_not hint (on behalf of cpaulin).coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7235 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15add a left and right tactic for classical logicnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7234 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13Détection d'un Fold incorrect suite à correction bug #986herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13Détection d'un Fold incorrect suite à correction bug #986herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7219 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19Documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7042 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵herbelin
aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-02Finalement, préservation de la compatibilité pour Z_lt_induction et ajout ↵herbelin
plutôt de nouveaux énoncés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6984 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-02Lemme de passage de l'autre côté d'une égalitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6983 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-26Fixed hypotheses of Z_lt_induction (see #957)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-31Added option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6903 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-29Missing translating a 'O' into a '0' (again - cf bug #947); removed useless ↵herbelin
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
2005-03-29Missing translating a 'O' into a '0' (again)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6897 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-24Missing translating a 'O' into a '0'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6884 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16MAJ PolyList -> Listherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6844 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-23quelques tactics ltacletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6773 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-07Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des ↵coq
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
2005-02-04Suppression de l'Unboxed des opérations sur positive (cf bug 898)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6676 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Essai d'utilisation de 'where' pour les notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6675 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6670 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03legere simplification des preuves de le_S_n et pred_leletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6669 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6666 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-19In_dec transparent (wish #902)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6483 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Inutile de réserver les notations à base de '{ }'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6410 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-05MAJ changements ChoiceFactsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6401 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-05Paramétrisation du domaine des axiomes de choix + ajout description = ↵herbelin
choice pour les propriétés décidables vers nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6399 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22compatibility with POWERPCgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-19Généralisation à Type de certaines propriétés des relationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6331 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16Copy of the definition of prodT (already in the standard library) removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6306 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-07MAJ commentaire sur incohérence EM dans Setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6281 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-02Réponse à la conjecture que PI est indépendant de EM dans CCherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6273 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-19Proof term size reduction (again).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6241 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18* Code simplification and clean-up. In particular there is no more codesacerdot
duplicated between add_relation and add_setoid. * Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v * Term size reduction (first part): when a relation is registered, we add to the environment a definition that gives back either the relation as an argument or as a relation class. The definition is used to reduce the term size. [ Note: we could save a bit more by defining two definitions in place of one. However, we suppose that the lambda term fragments generated can be shared quite effectively. Thus we would recive almost no benefit by sharing in terms of size. What about proof checking time? ] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6238 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵herbelin
evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07iff and impl are now declared as transitive relations.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6192 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06* New syntactic sugar: Add Relation ... transitivity proved by ...sacerdot
now declares both the relation and the relation as a morphism, computing the appropriate signature (depending on the reflexivity of the relation). * New parameter "as ..." to Add Relation (to be able to compute the morphism name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6189 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06added transitivitybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6188 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29impl is a reflexive relation (it used to be areflexive).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6154 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:22:20 +0000