aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* 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
* fichiers sur la ligne de commande passes a Coq IDEGravatar filliatr2003-03-03
* Ajout du traducteurGravatar desmettr2003-02-05
* interface GTK2 experimentaleGravatar monate2003-02-04
* changement de place du Initial State (maintenant apres l'analyse de la ligne ...Gravatar filliatr2003-01-30
* deplacement du test 'il reste des preuves en cours'Gravatar filliatr2003-01-20
* msg Failtac; echec -batch s'il reste des preuvesGravatar filliatr2003-01-17
* Ajout options -v7 et -v8, et commandes V7only et V8onlyGravatar herbelin2002-12-10
* Nouvelle option -xml à coqtop pour compiler un développement enGravatar herbelin2002-11-05
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* raccourci -l en plus de -load-vernac-sourceGravatar letouzey2002-03-07
* Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parceGravatar ddr2002-02-20
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Plusieurs arguments autorisés pour Require et Read ModuleGravatar herbelin2002-01-18
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05