index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Vers la fin de la restructuration
herbelin
2001-09-21
*
Problème d'affichage d'un . pour les Local_constraints; remplacement par Idtac
herbelin
2001-09-21
*
Mise en place globalisation optionnelle pour Infix/Distfix
herbelin
2001-09-21
*
Protection contre des arguments farfelus pour les implicites manuels
herbelin
2001-09-21
*
Protection contre Not_found
herbelin
2001-09-21
*
*** empty log message ***
mohring
2001-09-21
*
Mise a jour
mohring
2001-09-21
*
make doc
filliatr
2001-09-21
*
Amélioration affichage de print_leaf_entry
herbelin
2001-09-20
*
Rajout 'Set Printing Depth'
herbelin
2001-09-20
*
MAJ
herbelin
2001-09-20
*
Correction (double) bug de Generalize Dependent
herbelin
2001-09-20
*
Correction bug affichage Infix/Distfix
herbelin
2001-09-20
*
Transparent
barras
2001-09-20
*
MAJ V7.1
herbelin
2001-09-20
*
Nettoyage des commentaires
herbelin
2001-09-20
*
MAJ V7.1
herbelin
2001-09-20
*
Nettoyage des commentaires
herbelin
2001-09-20
*
Compatibilté make doc
herbelin
2001-09-20
*
Test inférence prédicat en présence d'univers
herbelin
2001-09-20
*
correction du eta_expanse
letouzey
2001-09-20
*
MAJ V7.1
herbelin
2001-09-20
*
Nombre magique pour la V7.1
herbelin
2001-09-20
*
Le prédicat du vieux Case ne doit pas contenir d'univers algébrique même q...
herbelin
2001-09-20
*
Report des modifs de Claudio
herbelin
2001-09-20
*
Pas de warning pour le -I . par défaut de Coq
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
*
warning silencieux
filliatr
2001-09-20
*
version V7.1
herbelin
2001-09-20
*
Restriction de l'avertissement add_loadpath au mode verbeux
herbelin
2001-09-20
*
On ignore les répertoires qui ne correspondent pas à des idents
herbelin
2001-09-20
*
On ignore les répertoires invisibles dans all_subdirs
herbelin
2001-09-20
*
Romega
mohring
2001-09-20
*
let-in dans Refine
filliatr
2001-09-20
*
Refine et let-in
filliatr
2001-09-20
*
Blindage, de peur que des types entrant non en forme normale ne provoque des ...
herbelin
2001-09-19
*
Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...
herbelin
2001-09-19
*
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...
herbelin
2001-09-19
*
Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ...
herbelin
2001-09-19
*
Intégration partielle des modifs de la V7.0
herbelin
2001-09-19
*
Affichage des dir_path vide
herbelin
2001-09-19
*
Autorisation de surcharge d'un -R par un -I
herbelin
2001-09-19
*
ajout du fichier CHANGES
letouzey
2001-09-19
*
la cible all était incomplète
filliatr
2001-09-19
*
Protection hd d'une liste vide
herbelin
2001-09-19
*
adaptation a la nouvelle syntaxe Extract Inlined Constant
letouzey
2001-09-19
*
Changements de Extraction truc et Recursive Extraction
letouzey
2001-09-19
*
make install dans coq_makefile et repertoire associe user-contrib ajoute au l...
filliatr
2001-09-19
[next]