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
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Typo message Scheme
herbelin
2001-02-28
*
bug Reset et Sections
filliatr
2001-02-28
*
Stringmap -> Idmap
herbelin
2001-02-22
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Prise en compte noms longs dans Implicits
herbelin
2001-02-16
*
Erreur sur commit
herbelin
2001-02-14
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
export a function that is needed in pcoq.
bertot
2001-02-13
*
Make sure the initial state used in a protected loop is the state chose exactly
bertot
2001-02-13
*
Theoreme opaques
mohring
2001-02-12
*
All errors were not well reported before. In particular syntax errors were
bertot
2001-02-10
*
Two pairs of parentheses were missing.
bertot
2001-02-09
*
option -m (utilisation memoire)
filliatr
2001-02-09
*
exported several functions that are used in the graphical interface pcoq.
bertot
2001-02-09
*
changed the design to have command groups executed in a protected manner
bertot
2001-02-09
*
Scratch par defaut si rien n'est specifier dans Add LoadPath
herbelin
2001-02-08
*
Suppression warning no .coqrc
herbelin
2001-02-08
*
export a function that can be used to retrieve the context corresponding
bertot
2001-02-08
*
Meilleure approche du conflit path/freeze/library_root en séquentialisant la...
herbelin
2001-02-07
*
Reparation du pretty-print pour les tactiques
delahaye
2001-02-07
*
Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir
herbelin
2001-02-07
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...
herbelin
2001-02-06
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
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
[next]