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
*
Reorganisation de Goption. Passage des options l'utilisant en synchrone
letouzey
2001-10-30
*
Oups: un relicat de fn de cache
letouzey
2001-10-29
*
Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...
letouzey
2001-10-26
*
correctif bug des de Bruijn du Double Case
letouzey
2001-10-25
*
seisme suite. correction bugs
letouzey
2001-10-24
*
Patch de goption.ml pour faire marcher les options synchrones. Passage des op...
letouzey
2001-10-24
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
suite du seisme
letouzey
2001-10-23
*
chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...
letouzey
2001-10-22
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
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
[next]