aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des jours...Gravatar coq2005-02-07
* Suppression de l'Unboxed des opérations sur positive (cf bug 898)Gravatar herbelin2005-02-04
* Essai d'utilisation de 'where' pour les notationsGravatar herbelin2005-02-04
* Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursGravatar herbelin2005-02-03
* legere simplification des preuves de le_S_n et pred_leGravatar letouzey2005-02-03
* Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursGravatar herbelin2005-02-03
* In_dec transparent (wish #902)Gravatar herbelin2004-12-19
* Inutile de réserver les notations à base de '{ }'Gravatar herbelin2004-12-06
* MAJ changements ChoiceFactsGravatar herbelin2004-12-05
* Paramétrisation du domaine des axiomes de choix + ajout description = choice...Gravatar herbelin2004-12-05
* compatibility with POWERPCGravatar gregoire2004-11-22
* Généralisation à Type de certaines propriétés des relationsGravatar herbelin2004-11-19
* Copy of the definition of prodT (already in the standard library) removed.Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* MAJ commentaire sur incohérence EM dans SetGravatar herbelin2004-11-07
* Réponse à la conjecture que PI est indépendant de EM dans CCGravatar herbelin2004-11-02
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Proof term size reduction (again).Gravatar sacerdot2004-10-19
* * Code simplification and clean-up. In particular there is no more codeGravatar sacerdot2004-10-18
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* iff and impl are now declared as transitive relations.Gravatar sacerdot2004-10-07
* * New syntactic sugar: Add Relation ... transitivity proved by ...Gravatar sacerdot2004-10-06
* added transitivityGravatar barras2004-10-06
* impl is a reflexive relation (it used to be areflexive).Gravatar sacerdot2004-09-29
* impl relation and impl/and/or/not morphisms over impl declared.Gravatar sacerdot2004-09-29
* * cleaning/renamingGravatar sacerdot2004-09-08
* The Coq part of the reflexive tactic is now able to handle alsoGravatar sacerdot2004-09-08
* * The Coq part of the reflexive tactic setoid_rewrite is generalized toGravatar sacerdot2004-09-07
* New reflexive implementation of setoid_rewrite. The new implementationGravatar sacerdot2004-09-03
* Zbool déjà dans ZArith_baseGravatar herbelin2004-08-03
* Minimisation utilisation NNPPGravatar herbelin2004-08-03
* Déclaration d'obsolescenceGravatar herbelin2004-08-03
* TypoGravatar herbelin2004-08-03
* RefGravatar herbelin2004-08-03
* Commentaires coqdocGravatar herbelin2004-08-01
* Commentaires coqdocGravatar herbelin2004-08-01
* Nouvelle en-têteGravatar herbelin2004-07-16
* simplified proof (eq and eqT are now the same)Gravatar barras2004-06-25
* Nouveaux thms de non circularité de natGravatar herbelin2004-06-02
* eq2eqT et eqT2eq devenus obsolètesGravatar herbelin2004-06-02
* sumbool et sumor affich avec 'if' si possibleGravatar herbelin2004-04-06
* CommentairesGravatar herbelin2004-03-29
* Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...Gravatar herbelin2004-03-28
* MAJ commentairesGravatar herbelin2004-03-24
* Definition de la notation de la paire par un motif recursifGravatar herbelin2004-03-17
* CommentairesGravatar herbelin2004-03-17
* ajout decimal_exp pour interpreter les notations decimalesGravatar mohring2004-03-12
* ide: silent behavior better, save icon, -byte worksGravatar marche2004-03-03
* MAJ CommentairesGravatar herbelin2004-02-28
* Ajout delimiteur pour bool_scopeGravatar herbelin2004-02-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 11:48:43 +0000