index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
maj
filliatr
2004-02-07
*
maj
filliatr
2004-02-07
*
MAJ
herbelin
2004-02-06
*
Test dependencies in constructors
herbelin
2004-02-06
*
correction de bugs de congruence et firstorder (inductifs)
corbinea
2004-02-06
*
Ajout filtrage sur motifs dépendants dans des inductifs différents
herbelin
2004-02-06
*
maj
filliatr
2004-02-06
*
On s'affranchit de l'information inductif ou pas dans le prédicat (càd
herbelin
2004-02-05
*
Suppression des types dans la signature du predicat (ils sont
herbelin
2004-02-05
*
maj
filliatr
2004-02-05
*
maj
filliatr
2004-02-05
*
Reconnaissance précoce de la dépendance du prédicat en un terme filtré
herbelin
2004-02-04
*
Vérification de la prise en compte des termes de type non inductif
herbelin
2004-02-04
*
clean-ide plus precis
herbelin
2004-02-04
*
Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...
herbelin
2004-02-04
*
Boite autour des quote pour eviter un retour a la ligne apres le premier guil...
herbelin
2004-02-04
*
bug fix find coqide
coq
2004-02-04
*
highlight
marche
2004-02-04
*
search window
coq
2004-02-04
*
maj
filliatr
2004-02-04
*
MAJ
herbelin
2004-02-03
*
Relachement condition pour afficher @ en cas d'explicitation d'implicites
herbelin
2004-02-03
*
Relachement condition pour declarer un inductif dans la table des 'If'; contr...
herbelin
2004-02-03
*
Backtrack sur recuperation de noms a partir du type, car casse la correction ...
herbelin
2004-02-03
*
Bug focus
herbelin
2004-02-03
*
Protection contre noms de variable indefinis et guillemets autour des constr
herbelin
2004-02-03
*
Politique de filtrage pour l'affichage plus coercitif pour les lieurs : un no...
herbelin
2004-02-03
*
maj
filliatr
2004-02-03
*
reorganize the order of librairies in the entry CMO to make sure this can
bertot
2004-02-02
*
adds the possibility to mark function arguments as formulas in Ltac
bertot
2004-02-02
*
adds the possibility to mark function arguments as formulas in Ltac
bertot
2004-02-02
*
maj
filliatr
2004-01-31
*
updates the definition of tactics using Ltac and adds the subst tactic
bertot
2004-01-30
*
adds module commands and update the extration command
bertot
2004-01-30
*
maj
filliatr
2004-01-30
*
maj
filliatr
2004-01-30
*
pour win32
coq
2004-01-29
*
Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...
herbelin
2004-01-29
*
Reparation d'une rupture (en presence de types implicites) de l'invariant que...
herbelin
2004-01-29
*
pour ide sous windows
coq
2004-01-29
*
MAJ
herbelin
2004-01-29
*
Suppression de 'Print.' en v8
herbelin
2004-01-29
*
Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...
herbelin
2004-01-29
*
updates the tactics contradiction and autorewrite, the commands
bertot
2004-01-29
*
maj
filliatr
2004-01-29
*
Bug de Require multiple
herbelin
2004-01-28
*
make sure that 'in' clauses for reduction tactics are translated
bertot
2004-01-28
*
maj
filliatr
2004-01-28
*
maj
filliatr
2004-01-28
*
Bug activation erronée du traducteur en v8
herbelin
2004-01-27
[next]