index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
Un ++ au lieu d'un ;
herbelin
2001-12-21
*
Corrections post contournement des streams avec ++
herbelin
2001-12-19
*
Nettoyage exceptions liées au vieux Case
herbelin
2001-12-18
*
Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...
herbelin
2001-12-16
*
compat ocaml 3.03
filliatr
2001-12-13
*
- condition de garde (suite)
barras
2001-12-10
*
reparation de Locate
barras
2001-11-29
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Amélioration message Cases
herbelin
2001-11-21
*
Amélioration messages d'erreur arité incorrecte (notamment record)
herbelin
2001-11-21
*
Prise en compte des '?' aussi dans le type des définitions
herbelin
2001-11-21
*
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-20
*
Code mort
herbelin
2001-11-20
*
Diverses petites simplications de la machine de preuves.
clrenard
2001-11-19
*
Mise en place d'une méthode directe pour indiquer le type des déclarations ...
herbelin
2001-11-19
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
Nettoyage coercions et classes
herbelin
2001-11-09
*
Choucroute entre les tables de synchronisation, les options -silent et les et...
letouzey
2001-11-08
*
corrections mineures suite au commit de restructuration du noyau
barras
2001-11-06
*
Suite de la suppression : enamed_declaration est remplace par evar_map.
clrenard
2001-11-06
*
Oops
barras
2001-11-05
*
GROS COMMIT:
barras
2001-11-05
*
Reorganisation de Goption. Passage des options l'utilisant en synchrone
letouzey
2001-10-30
*
Vérification précoce qu'un lemme n'existe pas déjà
herbelin
2001-10-26
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Amélioration mise en page Print ML Module et Print ML Module
herbelin
2001-10-17
*
Nettoyage Recordobj et conséquences
herbelin
2001-10-16
*
Orthographe
herbelin
2001-10-15
*
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-12
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Compatibilite Windoz
herbelin
2001-09-26
*
Le fichier .vo etait ecrit dans un mauvais repertoire si ce dernier etait tro...
herbelin
2001-09-26
*
Commentaires pour make doc
herbelin
2001-09-24
*
Réparation des options Set Printing and co
herbelin
2001-09-21
*
Mise en place globalisation optionnelle pour Infix/Distfix
herbelin
2001-09-21
*
Protection contre Not_found
herbelin
2001-09-21
*
Correction bug affichage Infix/Distfix
herbelin
2001-09-20
*
Transparent
barras
2001-09-20
*
On ignore les répertoires qui ne correspondent pas à des idents
herbelin
2001-09-20
*
Protection hd d'une liste vide
herbelin
2001-09-19
*
make install dans coq_makefile et repertoire associe user-contrib ajoute au l...
filliatr
2001-09-19
*
Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...
herbelin
2001-09-19
*
Mise en place de noms contenant la section pour Fact et Remark
herbelin
2001-09-18
*
Ajout d'une option et d'une fonction compile pour fabriquer les .vo
herbelin
2001-09-18
*
Suppression du message d'erreur si une coercion mettant en jeu des locaux n'e...
herbelin
2001-09-18
*
Bug discharge d'une déclaration de coercion pour une constante non définie ...
herbelin
2001-09-18
*
Blindage de Show Intro
letouzey
2001-09-17
*
Transformation de Remark/Fact en constantes non visibles sans qualification
herbelin
2001-09-14
[next]