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-12-18
ote les redondances des entetes
letouzey
2001-12-17
le save de Correctness faisant assert false
barras
2001-12-13
compat ocaml 3.03
filliatr
2001-12-10
correction de bugs concernant la gestion des modules. debranchement du test d...
letouzey
2001-11-29
nouvel algo de conversion plus uniforme
barras
2001-11-21
remise au gout du jour du repertoire theories/Sorting de la V6.3
letouzey
2001-11-21
Make sure that NatRing won't loop forever.
bertot
2001-11-20
hack temporaire concernant les remarks/modules
letouzey
2001-11-20
iota généralisé
letouzey
2001-11-20
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-19
Mise en place d'une méthode directe pour indiquer le type des déclarations ...
herbelin
2001-11-19
Renommage qualid_of_global en shortest_qualid_of_global
herbelin
2001-11-14
oubli: changement de nil en nilT
mayero
2001-11-14
Changement de list en listT, cons en consT et app en appT
mayero
2001-11-14
Revolution culturelle: suppression des arguments prop
letouzey
2001-11-13
Moins de fichiers avec des axioms
letouzey
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
[prev]
[next]