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
*
compat ocaml 3.03
filliatr
2001-12-13
*
correction de bugs concernant la gestion des modules. debranchement du test d...
letouzey
2001-12-10
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
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-21
*
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-20
*
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-19
*
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-14
*
Moins de fichiers avec des axioms
letouzey
2001-11-13
*
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-12
*
typo
letouzey
2001-11-09
*
Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs...
letouzey
2001-11-08
*
epsilon
letouzey
2001-11-08
*
Refonte du fichier mlutil.ml. Correction d'un bug d'optim case
letouzey
2001-11-07
*
suite des tests
letouzey
2001-11-06
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
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-05
*
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-03
*
suite des modifs concernant les optimisations divers
letouzey
2001-11-02
*
les fixpoints sont de nouveau bien optimisés
letouzey
2001-11-01
*
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-31
*
legeres modifs pretty-print de l'extractions
letouzey
2001-10-30
*
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
[next]