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
*
- 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
*
Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...
herbelin
2001-09-10
*
Mécanisme pour faire remonter les contraintes de typage sur les variables de...
herbelin
2001-09-09
*
Suppression des library roots, on teste si un nom est absolu autrement
herbelin
2001-09-07
*
Bug default module name (2eme)
herbelin
2001-09-06
*
Parsing
herbelin
2001-08-10
*
anomaly -> error
clrenard
2001-07-10
[next]