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
*
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
*
Ref
herbelin
2004-08-03
*
Commentaires coqdoc
herbelin
2004-08-01
*
Commentaires coqdoc
herbelin
2004-08-01
*
Nouvelle en-tête
herbelin
2004-07-16
*
simplified proof (eq and eqT are now the same)
barras
2004-06-25
*
Nouveaux thms de non circularité de nat
herbelin
2004-06-02
*
eq2eqT et eqT2eq devenus obsolètes
herbelin
2004-06-02
*
sumbool et sumor affich avec 'if' si possible
herbelin
2004-04-06
*
Commentaires
herbelin
2004-03-29
*
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2004-03-28
*
MAJ commentaires
herbelin
2004-03-24
*
Definition de la notation de la paire par un motif recursif
herbelin
2004-03-17
*
Commentaires
herbelin
2004-03-17
*
ajout decimal_exp pour interpreter les notations decimales
mohring
2004-03-12
*
ide: silent behavior better, save icon, -byte works
marche
2004-03-03
*
MAJ Commentaires
herbelin
2004-02-28
*
Ajout delimiteur pour bool_scope
herbelin
2004-02-12
*
Décomposition automatique des règles d'analyse syntaxique pour les
herbelin
2004-02-12
*
backtrack implicit dans Bvector
marche
2004-02-10
*
patch Bvector: args implicites
marche
2004-02-09
*
MAJ simplification
herbelin
2004-01-27
*
Suppression de Rsyntax en v8
herbelin
2004-01-13
*
bugs avec Pose et Assert
barras
2004-01-09
[next]