aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
Commit message (Expand)AuthorAge
* minor bugfixes. CoqIde development will resume soon now ...Gravatar vgross2009-05-13
* - per session coq command stackGravatar vgross2009-03-07
* fixed groebner as a plugin + pattern matching TimeoutGravatar barras2009-03-06
* Temporary hack to make coqide.byte work (backport r11948) (see #2062)Gravatar glondu2009-03-04
* Report des revisions #11826, #11828 et #11829 de v8.2 vers trunkGravatar notin2009-02-11
* DISCLAIMERGravatar puech2009-01-17
* Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...Gravatar notin2009-01-06
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Native "Declare ML Module" when possibleGravatar glondu2008-10-28
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
* - Rebranchement backtrack du langage déclaratif dans CoqideGravatar herbelin2008-07-18
* Bug résiduel du backtrack de coqide se produisant lorsque la limite deGravatar herbelin2008-07-10
* Encore une suite au 11188/11193 (c'était pas un bon jour)Gravatar herbelin2008-07-01
* CoqIDE: 2 problèmes de undo encore:Gravatar herbelin2008-06-13
* Plutôt que de reposer sur le vernacexpr pour détecter les débuts deGravatar herbelin2008-06-11
* On prend des risques en tentant d'optimiser encore plus le undo en casGravatar herbelin2008-06-09
* - On adopte finalement la méthode de Pierre Courtieu pour le undo deGravatar herbelin2008-06-06
* - Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"Gravatar herbelin2008-05-30
* Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image deGravatar herbelin2008-05-28
* Réorganisation des points d'appui du undo de CoqIDE (type reset_info).Gravatar herbelin2008-05-26
* Bug undo CoqIDE sur EndGravatar herbelin2008-05-26
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
* - Prise en compte des frozen state de Coq autant que possible pourGravatar herbelin2008-05-24
* Léger backtrack sur commit coqide précédent (si la commande à annulerGravatar herbelin2008-05-20
* Amélioration de la colorisation, du backtrack et des messages de CoqIDEGravatar herbelin2008-05-10
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* add visibility of extraction messages in coqideGravatar letouzey2007-10-16
* Bug 1716: Scheme now print the right messagesGravatar vsiles2007-10-04
* fin des conclusions multiplesGravatar corbinea2007-04-26
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* decl mode: anonymous factsGravatar corbinea2007-01-25
* fixed same_file (#1141)Gravatar barras2006-10-23
* coqide: affichage des sous-buts et hypothèses et métas comme types deGravatar herbelin2006-10-19
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Suite commit 9110 (uniformisation position notation dans les blocs inductifs)Gravatar herbelin2006-09-01
* Modifications dans les scripts de configuration (coqtop et coqide affichent m...Gravatar notin2006-07-28
* Remplacement VernacDebug par VernacSetOption (suite)Gravatar herbelin2006-07-06
* Changement de l'option -where: on vérifie si la variable d'environnement COQ...Gravatar notin2006-06-07
* Correction bug #990 (LoadPath et option -R de coqideGravatar notin2006-05-30
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* bug de coqide sous windows (bad file descriptor)Gravatar barras2005-11-23
* Types inductifs parametriquesGravatar mohring2005-11-02
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* ide: silent behavior better, save icon, -byte worksGravatar marche2004-03-03