index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernac.ml
Commit message (
Expand
)
Author
Age
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
*
Protection table des locations lors de Load (pour coqdoc)
herbelin
2004-01-22
*
*** empty log message ***
barras
2003-12-24
*
Bug: faut brancher la sortie des tactiques sur stdout pendant traduction
herbelin
2003-11-18
*
Mise en place traduction des tactiques apres evaluation pour permettre des ch...
herbelin
2003-11-09
*
bug traduction de auto.(simpl). en auto.simpl.
barras
2003-10-20
*
oups! ca compile maintenant
barras
2003-10-16
*
translator avoids printing a . followed by a ( by inserting a space
barras
2003-10-16
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait
herbelin
2003-10-03
*
Traduction aussi si -translate et -load-vernac-source
herbelin
2003-09-24
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Plutôt que de faire "Load" silencieusement, en profiter pour traduire
herbelin
2003-09-18
*
Pour cacher le contenu de Load au traducteur
herbelin
2003-09-16
*
Debranchement du traducteur pour Load !
herbelin
2003-09-10
*
Freeze mal place
herbelin
2003-09-02
*
Bug et amliorations diverses
herbelin
2003-08-12
*
Ajout systématique de Proof dans la traduction
herbelin
2003-06-23
*
Possibilité de syntaxe conjointement à la définition des inductifs et des ...
herbelin
2003-05-21
*
Affichage commentaires
herbelin
2003-05-13
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Bug fermeture de stdout
herbelin
2003-04-29
*
Formattage affichage
herbelin
2003-04-09
*
Mécanisme plus simple et efficace pour traduire les implicites
herbelin
2003-04-09
*
Bugs synchronisation pour gestion traduction des implicites
herbelin
2003-04-09
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
*** empty log message ***
barras
2003-03-12
*
Recuperation des outputs de l'interpretation des commandes vernac et des erre...
desmettr
2003-02-28
*
Undo dans Coq IDE
filliatr
2003-02-11
*
Ajout du traducteur
desmettr
2003-02-05
*
deplacement du test 'il reste des preuves en cours'
filliatr
2003-01-20
*
Ajout options -v7 et -v8, et commandes V7only et V8only
herbelin
2002-12-10
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Error_in_file redondant et inapproprié
herbelin
2002-07-11
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
compat ocaml 3.03
filliatr
2001-12-13
*
- condition de garde (suite)
barras
2001-12-10
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
corrections mineures suite au commit de restructuration du noyau
barras
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Le fichier .vo etait ecrit dans un mauvais repertoire si ce dernier etait tro...
herbelin
2001-09-26
*
Ajout d'une option et d'une fonction compile pour fabriquer les .vo
herbelin
2001-09-18
*
nettoyage d'entrees de grammaires inutiles
courant
2001-04-09
*
entetes
filliatr
2001-03-15
*
Import module force l'ouverture du module même s'il était déjà ouvert afi...
herbelin
2000-12-20
*
Une capsule pour save_module_to dans Discharge
herbelin
2000-11-20
*
nouveau load path
filliatr
2000-11-08
[next]