index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
coqtop.ml
Commit message (
Expand
)
Author
Age
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
option -no-hash-consing pour supprimmer le hash-consing
filliatr
2004-10-12
*
Bug List.hd vs list_last
herbelin
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
bug #780: compilation of several units in the same coqtop process
barras
2004-07-13
*
Affichage de la date de checkout même si pas dans le répertoire de compilation
herbelin
2004-05-26
*
Nom qualifié pour option -top
herbelin
2004-03-28
*
Ajout option -top pour changer le nom 'Top' du toplevel
herbelin
2004-03-28
*
ide: silent behavior better, save icon, -byte works
marche
2004-03-03
*
- fixed the Assert_failure error in kernel/modops
barras
2004-02-18
*
Ajout load-vernac-source-verbose
herbelin
2004-01-15
*
ameliorations coqide
coq
2003-12-30
*
Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7...
herbelin
2003-11-29
*
Utilisation de la date cvs dans l'en-tete si make.result existe
herbelin
2003-11-18
*
Suppression StronglyClassical, StronglyConstructive devient plus concretement...
herbelin
2003-11-08
*
Interdiction de nommer un object de nom commencant par Coq en dehors de la bi...
herbelin
2003-11-01
*
Options -strongly-constructive et -strongly-classical
herbelin
2003-10-28
*
translate_file etait abusivement positionne
herbelin
2003-10-11
*
Renommage no-strict en -strict-implicit; option -dont-load-proofs
herbelin
2003-10-08
*
Traduction aussi si -translate et -load-vernac-source
herbelin
2003-09-24
*
Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...
herbelin
2003-09-12
*
Fusion -translate et -ftranslate
herbelin
2003-08-14
*
Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofs
herbelin
2003-08-11
*
coqide: .* on start/add \n on eof
monate
2003-05-14
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Ajout option -v8 à coqtopnew pour permettre le changement de comportement de...
herbelin
2003-04-09
*
Prise en compte affichage coercions traducteur dans Constrextern
herbelin
2003-04-09
*
*** empty log message ***
barras
2003-03-12
*
tous les fichiers passes a Coq IDE
filliatr
2003-03-04
*
fichiers sur la ligne de commande passes a Coq IDE
filliatr
2003-03-03
*
Ajout du traducteur
desmettr
2003-02-05
*
interface GTK2 experimentale
monate
2003-02-04
*
changement de place du Initial State (maintenant apres l'analyse de la ligne ...
filliatr
2003-01-30
*
deplacement du test 'il reste des preuves en cours'
filliatr
2003-01-20
*
msg Failtac; echec -batch s'il reste des preuves
filliatr
2003-01-17
*
Ajout options -v7 et -v8, et commandes V7only et V8only
herbelin
2002-12-10
*
Nouvelle option -xml à coqtop pour compiler un développement en
herbelin
2002-11-05
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
raccourci -l en plus de -load-vernac-source
letouzey
2002-03-07
*
Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce
ddr
2002-02-20
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
compat ocaml 3.03
filliatr
2001-12-13
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Compatibilite Windoz
herbelin
2001-09-26
*
Ajout d'une option et d'une fonction compile pour fabriquer les .vo
herbelin
2001-09-18
[next]