index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
changement parametres inductifs dans les theories
mohring
2005-11-30
*
*** empty log message ***
letouzey
2005-08-26
*
Fix sumbool_not hint (on behalf of cpaulin).
coq
2005-07-15
*
add a left and right tactic for classical logic
narboux
2005-07-15
*
Détection d'un Fold incorrect suite à correction bug #986
herbelin
2005-07-13
*
Détection d'un Fold incorrect suite à correction bug #986
herbelin
2005-07-13
*
Documentation
herbelin
2005-05-19
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...
herbelin
2005-05-02
*
Lemme de passage de l'autre côté d'une égalité
herbelin
2005-05-02
*
Fixed hypotheses of Z_lt_induction (see #957)
herbelin
2005-04-26
*
Added option_map
herbelin
2005-03-31
*
Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...
herbelin
2005-03-29
*
Missing translating a 'O' into a '0' (again)
herbelin
2005-03-29
*
Missing translating a 'O' into a '0'
herbelin
2005-03-24
*
MAJ PolyList -> List
herbelin
2005-03-16
*
quelques tactics ltac
letouzey
2005-02-23
*
Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des jours...
coq
2005-02-07
*
Suppression de l'Unboxed des opérations sur positive (cf bug 898)
herbelin
2005-02-04
*
Essai d'utilisation de 'where' pour les notations
herbelin
2005-02-04
*
Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs
herbelin
2005-02-03
*
legere simplification des preuves de le_S_n et pred_le
letouzey
2005-02-03
*
Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs
herbelin
2005-02-03
*
In_dec transparent (wish #902)
herbelin
2004-12-19
*
Inutile de réserver les notations à base de '{ }'
herbelin
2004-12-06
*
MAJ changements ChoiceFacts
herbelin
2004-12-05
*
Paramétrisation du domaine des axiomes de choix + ajout description = choice...
herbelin
2004-12-05
*
compatibility with POWERPC
gregoire
2004-11-22
*
Généralisation à Type de certaines propriétés des relations
herbelin
2004-11-19
*
Copy of the definition of prodT (already in the standard library) removed.
sacerdot
2004-11-16
*
Changement dans les boxed values .
gregoire
2004-11-12
*
MAJ commentaire sur incohérence EM dans Set
herbelin
2004-11-07
*
Réponse à la conjecture que PI est indépendant de EM dans CC
herbelin
2004-11-02
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Proof term size reduction (again).
sacerdot
2004-10-19
*
* Code simplification and clean-up. In particular there is no more code
sacerdot
2004-10-18
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
iff and impl are now declared as transitive relations.
sacerdot
2004-10-07
*
* New syntactic sugar: Add Relation ... transitivity proved by ...
sacerdot
2004-10-06
*
added transitivity
barras
2004-10-06
*
impl is a reflexive relation (it used to be areflexive).
sacerdot
2004-09-29
*
impl relation and impl/and/or/not morphisms over impl declared.
sacerdot
2004-09-29
*
* cleaning/renaming
sacerdot
2004-09-08
*
The Coq part of the reflexive tactic is now able to handle also
sacerdot
2004-09-08
*
* The Coq part of the reflexive tactic setoid_rewrite is generalized to
sacerdot
2004-09-07
*
New reflexive implementation of setoid_rewrite. The new implementation
sacerdot
2004-09-03
*
Zbool déjà dans ZArith_base
herbelin
2004-08-03
*
Minimisation utilisation NNPP
herbelin
2004-08-03
*
Déclaration d'obsolescence
herbelin
2004-08-03
*
Typo
herbelin
2004-08-03
[next]