index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
cc
Commit message (
Expand
)
Author
Age
*
Declarative language: fixed the generation of fixpoints for induction proofs.
corbinea
2007-07-24
*
fixed (PR#1483)
corbinea
2007-05-24
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
added congruence improvement
corbinea
2006-09-19
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Types inductifs parametriques
mohring
2005-11-02
*
new congruence
corbinea
2005-08-17
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
Uniformisation de destApplication en destApp
herbelin
2005-02-12
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2005-01-14
*
Nouvelle en-tête
herbelin
2004-07-16
*
oops
corbinea
2004-03-15
*
minor changes
corbinea
2004-03-14
*
congruence now handles disequalities
corbinea
2004-03-14
*
correction de bugs de congruence et firstorder (inductifs)
corbinea
2004-02-06
*
bugs avec Pose et Assert
barras
2004-01-09
*
cc update
corbinea
2003-12-09
*
error messages adjustement
corbinea
2003-12-02
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
ground->firstorder, cc-> congruence, CC final commit
corbinea
2003-11-29
*
just forgot something in previous commit
corbinea
2003-11-26
*
removal of CC.v lemata in cc (deprecated)
corbinea
2003-11-26
*
CC: added injection theory
corbinea
2003-11-25
*
Code simplification in CC
corbinea
2003-11-20
*
Cacher les .v8
herbelin
2003-10-03
*
Ground and CCsolve updates
corbinea
2003-05-25
*
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2003-03-31
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Adding the congruence closure tactics (CC and CCsolve).
corbinea
2002-10-01