aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* 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
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Compatibilite WindozGravatar herbelin2001-09-26
* Ajout d'une option et d'une fonction compile pour fabriquer les .voGravatar herbelin2001-09-18
* Bug default module name (2eme)Gravatar herbelin2001-09-06
* ParsingGravatar herbelin2001-08-10
* option -qualityGravatar filliatr2001-05-28
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* -boot n'implique plus -batchGravatar filliatr2001-04-19
* *** empty log message ***Gravatar courant2001-04-19
* utilisation de Options.if_verboseGravatar filliatr2001-04-03
* entetesGravatar filliatr2001-03-15
* bug Reset et SectionsGravatar filliatr2001-02-28
* option -m (utilisation memoire)Gravatar filliatr2001-02-09
* Meilleure approche du conflit path/freeze/library_root en séquentialisant la...Gravatar herbelin2001-02-07