aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* Suite ajout option -output-contextGravatar herbelin2006-12-08
* Ajout d'une option -output-context qui affiche le contexte en CCI pur à laGravatar herbelin2006-12-08
* Added a new option -emacs-U changing emacs prompt delimiters byGravatar courtieu2006-09-29
* Corrections mineuresGravatar notin2006-09-25
* Modifications dans les scripts de configuration (coqtop et coqide affichent m...Gravatar notin2006-07-28
* Ajout d'une option -with-geoproof à la configuration et à l'exécutionGravatar notin2006-06-09
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...Gravatar notin2006-06-08
* Réparation coqtop.mlGravatar notin2006-06-07
* Changement de l'option -where: on vérifie si la variable d'environnement COQ...Gravatar notin2006-06-07
* Modification of emacs output: Pp.warning and al now output warningGravatar courtieu2006-04-27
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement de stratégie vis à vis du positionnement du module Top en mode b...Gravatar herbelin2005-12-24
* option '-top dir' now works also in batch mode (2ème)Gravatar herbelin2005-12-22
* option '-top dir' now works also in batch mode; it is even necessary to ensur...Gravatar herbelin2005-12-22
* Changement des named_contextGravatar gregoire2005-12-02
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* compatibility with POWERPCGravatar gregoire2004-11-22
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* option -no-hash-consing pour supprimmer le hash-consingGravatar filliatr2004-10-12
* Bug List.hd vs list_lastGravatar herbelin2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* bug #780: compilation of several units in the same coqtop processGravatar barras2004-07-13
* Affichage de la date de checkout même si pas dans le répertoire de compilationGravatar herbelin2004-05-26
* Nom qualifié pour option -topGravatar herbelin2004-03-28
* Ajout option -top pour changer le nom 'Top' du toplevelGravatar herbelin2004-03-28
* ide: silent behavior better, save icon, -byte worksGravatar marche2004-03-03
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* Ajout load-vernac-source-verboseGravatar herbelin2004-01-15
* ameliorations coqideGravatar coq2003-12-30
* Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7...Gravatar herbelin2003-11-29
* Utilisation de la date cvs dans l'en-tete si make.result existeGravatar herbelin2003-11-18
* Suppression StronglyClassical, StronglyConstructive devient plus concretement...Gravatar herbelin2003-11-08
* Interdiction de nommer un object de nom commencant par Coq en dehors de la bi...Gravatar herbelin2003-11-01
* Options -strongly-constructive et -strongly-classicalGravatar herbelin2003-10-28
* translate_file etait abusivement positionneGravatar herbelin2003-10-11
* Renommage no-strict en -strict-implicit; option -dont-load-proofsGravatar herbelin2003-10-08
* Traduction aussi si -translate et -load-vernac-sourceGravatar herbelin2003-09-24
* Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...Gravatar herbelin2003-09-12
* Fusion -translate et -ftranslateGravatar herbelin2003-08-14
* Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofsGravatar herbelin2003-08-11
* coqide: .* on start/add \n on eofGravatar monate2003-05-14
* Factorisation des produits de même type; parenthèses autour des x:=c et n:=...Gravatar herbelin2003-04-29
* Ajout option -v8 à coqtopnew pour permettre le changement de comportement de...Gravatar herbelin2003-04-09
* Prise en compte affichage coercions traducteur dans ConstrexternGravatar herbelin2003-04-09
* *** empty log message ***Gravatar barras2003-03-12
* tous les fichiers passes a Coq IDEGravatar filliatr2003-03-04