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
*
Bug lié au discharge
herbelin
2001-01-31
*
Ajout option Set/Unset/Test Printing Coercions
herbelin
2001-01-31
*
Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...
herbelin
2001-01-31
*
Branchement sur Objdef
herbelin
2001-01-30
*
Les Objdef introduisent une convertibilité avec les projections dans le test...
herbelin
2001-01-30
*
backtrack sur le lexeur de la V6
filliatr
2001-01-30
*
pas de warning avec Opaque quand is_silent
filliatr
2001-01-29
*
make doc
herbelin
2001-01-27
*
Ré-introduction des implicites à la volée dans la définition des inductifs
herbelin
2001-01-27
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Réorganisation suite ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Bug Identity Coercion
herbelin
2001-01-18
*
Meta Definition + Tactic Definition
delahaye
2001-01-09
*
Arite cachee de Match Context + Meta Definition
delahaye
2001-01-05
*
Let doit etre utilise dans le mode de preuve
delahaye
2001-01-03
*
Rattrapage d'erreur pour le Case + Eval Compute in pour Definition
delahaye
2001-01-03
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
Bug installation non locale
herbelin
2000-12-27
*
Bug discharge process_class
herbelin
2000-12-25
*
Un nom long pour les variables de section qui font classe ou coercion; réorg...
herbelin
2000-12-25
*
Import module force l'ouverture du module même s'il était déjà ouvert afi...
herbelin
2000-12-20
*
correction de bugs sur commit précédent
herbelin
2000-12-19
*
Découpage des différentes fonctionnalités de build_mutual et definition_st...
herbelin
2000-12-19
*
Amélioration message d'erreur mauvais prédicat
herbelin
2000-12-18
*
Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite
herbelin
2000-12-16
*
- suppression mind_extract_params
filliatr
2000-12-15
*
Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...
herbelin
2000-12-15
*
Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...
herbelin
2000-12-15
*
Printer
mohring
2000-12-15
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
Amélioration message d'erreur
herbelin
2000-12-14
*
Raffinement erreur Wrong Predicate
herbelin
2000-12-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silent
filliatr
2000-12-12
*
Ajout erreur DoesNotOccurIn
herbelin
2000-12-06
*
Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...
herbelin
2000-12-06
*
Reparation conditions de positivites inductifs, echange dans add_entry
mohring
2000-12-06
*
Mini-nettoyage noms longs
herbelin
2000-12-05
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
Changement de la syntaxe des options -I et -R
herbelin
2000-11-30
*
Bug option -I et -R quand le répertoire est '..'
herbelin
2000-11-29
*
Bug option -I et -R quand le répertoire est '.'
herbelin
2000-11-29
*
Suppression cast inutile
herbelin
2000-11-29
*
Now AddRecPath and AddPath can be used with an As option to specify the
sacerdot
2000-11-29
*
load_path_entry structure simplified; field relative_subdir renamed to coq_di...
sacerdot
2000-11-29
*
Ajout d'une option d'alias à -I
herbelin
2000-11-29
*
Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...
herbelin
2000-11-29
*
Remplacement des add_include par add_rec_include pour avoir le repertoire dan...
herbelin
2000-11-28
[next]