index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
Age
Commit message (
Expand
)
Author
2001-11-12
Suppression des stamps et donc des *_constraints
clrenard
2001-11-12
suite du petit oups
letouzey
2001-11-12
petit oups
letouzey
2001-11-12
suite refonte extraction.ml
letouzey
2001-11-12
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
letouzey
2001-11-09
typo
letouzey
2001-11-08
Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs...
letouzey
2001-11-08
epsilon
letouzey
2001-11-07
Refonte du fichier mlutil.ml. Correction d'un bug d'optim case
letouzey
2001-11-06
suite des tests
letouzey
2001-11-06
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-05
refonte du test
letouzey
2001-11-05
optimisation consistant a parfois permuter case et fun
letouzey
2001-11-05
optim: Idset au lieu de list
letouzey
2001-11-05
GROS COMMIT:
barras
2001-11-05
message non barbare si extraction dans une section
letouzey
2001-11-03
changement epsilonesque
letouzey
2001-11-03
retablissement de l'optim case constant
letouzey
2001-11-03
ajout du script qualify2open qui met des open Truc en debut de fichier
letouzey
2001-11-03
Creation de Recursive Extarction Module
letouzey
2001-11-02
suite des modifs concernant les optimisations divers
letouzey
2001-11-01
les fixpoints sont de nouveau bien optimisés
letouzey
2001-10-31
suite de l'optimisation des Fix
letouzey
2001-10-31
correction du debut d'optimisation du Fix
letouzey
2001-10-31
multiples bricoles. Cf mon TODO papier
letouzey
2001-10-30
legeres modifs pretty-print de l'extractions
letouzey
2001-10-30
Reorganisation de Goption. Passage des options l'utilisant en synchrone
letouzey
2001-10-29
Oups: un relicat de fn de cache
letouzey
2001-10-26
Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...
letouzey
2001-10-25
correctif bug des de Bruijn du Double Case
letouzey
2001-10-24
seisme suite. correction bugs
letouzey
2001-10-24
Patch de goption.ml pour faire marcher les options synchrones. Passage des op...
letouzey
2001-10-23
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
suite du seisme
letouzey
2001-10-22
chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...
letouzey
2001-10-17
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-12
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-12
reparation
filliatr
2001-10-09
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-01
correction de deux petits bugs: case_identité trop fort et Anomaly dans le t...
letouzey
2001-09-21
Correction due au changement de semantique de Match
delahaye
2001-09-20
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-19
ajout du fichier CHANGES
letouzey
2001-09-19
adaptation a la nouvelle syntaxe Extract Inlined Constant
letouzey
[next]