index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-12
*
reparation
filliatr
2001-10-12
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
correction de deux petits bugs: case_identité trop fort et Anomaly dans le t...
letouzey
2001-10-01
*
Correction due au changement de semantique de Match
delahaye
2001-09-21
*
Transparent
barras
2001-09-20
*
correction du eta_expanse
letouzey
2001-09-20
*
Report des modifs de Claudio
herbelin
2001-09-20
*
bug affichage des termes ml fournis
letouzey
2001-09-20
*
utilisation du nouveau get_sort_family_of
letouzey
2001-09-20
*
changements mineurs du test
letouzey
2001-09-20
*
Romega
mohring
2001-09-20
*
ajout du fichier CHANGES
letouzey
2001-09-19
*
adaptation a la nouvelle syntaxe Extract Inlined Constant
letouzey
2001-09-19
*
Changements de Extraction truc et Recursive Extraction
letouzey
2001-09-19
*
Deux nouvelles optimisations pour Cases
letouzey
2001-09-19
*
MAJ V7.1
herbelin
2001-09-19
*
Verification supplementaire avant optimisation singleton
letouzey
2001-09-19
*
reparation Zne
mohring
2001-09-19
*
travail sur le Extract Constant
letouzey
2001-09-18
*
Modification de l'emplacement des fichiers pour les setoides.
clrenard
2001-09-18
*
Romega/names/Makefile
mohring
2001-09-18
*
MAJ vis à vis de la nouvelle non-localité des Remark/Fact
herbelin
2001-09-14
*
*** empty log message ***
mohring
2001-09-12
*
changement du make depend en vu du make reals
letouzey
2001-09-10
*
bug de rename_global modulaire corrige'
letouzey
2001-09-10
*
Nettoyage reduce_to_ind et one_step_reduce
herbelin
2001-09-09
*
Prsing
herbelin
2001-08-10
*
Parsing
herbelin
2001-08-10
*
Passage au nouveau Destruct
herbelin
2001-08-07
*
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-08-05
*
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-21
*
Ajout de la contrib sur les graphes
mohring
2001-07-18
*
Setoid_rewrite -> Rewrite
clrenard
2001-07-10
*
Ajout des fichiers pour le Ring pour setoides
clrenard
2001-07-10
*
Changement de place de la tactique Setoid_rewrite
clrenard
2001-07-10
*
Ajout d'un Ring pour setoides
clrenard
2001-07-10
*
correction bug Omega
filliatr
2001-07-05
*
Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...
herbelin
2001-07-02
*
Nettoyage/restructuration des ensembles d'indicateurs de réductions
herbelin
2001-07-02
*
Reduction du terme preuve fourni par Field
delahaye
2001-06-27
*
correction d'un bug de Correctness (pour Y Bertot)
filliatr
2001-06-27
*
Reduction tres significative du terme preuve
delahaye
2001-06-27
*
Les tacticques Setoid_replace/rewrite peuvent maintenant reecrire sous une
clrenard
2001-06-26
*
Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...
herbelin
2001-06-25
*
liste des equiv exportee
clrenard
2001-06-25
*
2 bugs: typevarlist pour inductifs + args pour flexibles
letouzey
2001-06-22
*
Ajout d'un Setoid_rewrite et meilleure resolution des petits sous-buts géné...
clrenard
2001-06-20
*
Un bug corrige.
clrenard
2001-06-19
*
Ajout de la tactique Setoid_replace.
clrenard
2001-06-12
[next]