aboutsummaryrefslogtreecommitdiff
path: root/ide/coq.mli
AgeCommit message (Expand)Author
2010-02-26New backtracking code + fix bug #2082.vgross
2010-02-26Introducing a dual stack setupvgross
2010-02-26New API for backtracking.vgross
2010-02-26Redispatch of printing tweaking hooks.vgross
2010-02-12Simplify backtrackingvgross
2010-02-12Refactoring of the printing optionsvgross
2010-01-11Revert "Isolation of proof-displaying code"vgross
2010-01-11Isolation of proof-displaying codevgross
2009-12-11Deport the backtracking code out of the idevgross
2009-12-03Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1vgross
2009-11-19Refactoring of coqide backtrack code, with the intent to put everythingvgross
2009-10-05Revert "kills the old backtracking framework and replaces it with"vgross
2009-09-29kills the old backtracking framework and replaces it withvgross
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-06-22clearing unused functionsvgross
2009-06-11Simplifying the call to print_no_goals and not calling it when no goalherbelin
2009-06-07Partial simplification of undo mechanism, relying only on Courtieu'sherbelin
2009-05-27keeping interface synch'edvgross
2008-06-13CoqIDE: 2 problèmes de undo encore:herbelin
2008-06-11Plutôt que de reposer sur le vernacexpr pour détecter les débuts deherbelin
2008-06-09On prend des risques en tentant d'optimiser encore plus le undo en casherbelin
2008-06-06- On adopte finalement la méthode de Pierre Courtieu pour le undo deherbelin
2008-05-28Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image deherbelin
2008-05-26Réorganisation des points d'appui du undo de CoqIDE (type reset_info).herbelin
2008-05-25- Nouvelle option "Set Printing Existential Instances" pour forcerherbelin
2008-05-24- Prise en compte des frozen state de Coq autant que possible pourherbelin
2008-05-10Amélioration de la colorisation, du backtrack et des messages de CoqIDEherbelin
2008-05-08** Efficacité, bugs, robustesse CoqIDE **herbelin
2007-04-26fin des conclusions multiplescorbinea
2006-09-20Declarative Proof Language: main commitcorbinea
2006-05-30Correction bug #990 (LoadPath et option -R de coqidenotin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-07-18Abstraction vis a vis du type loc pour ocaml 3.08herbelin
2004-07-16Nouvelle en-têteherbelin
2004-03-03ide: silent behavior better, save icon, -byte worksmarche
2003-09-19Coqide : les nouveaute d'aoutmonate
2003-07-16coqide: fixed problems with -R -I and coqide interactionmonate
2003-06-25coqide : status bar more informative, forbid Section/Module in proo modemonate
2003-06-13CoqIDE: undo immediat sur les commandes ne modifiant pas l'etatfilliatr
2003-05-26coqide: blaster interruptiblemonate
2003-05-22coqide: blaster V1monate
2003-05-07coqide: toolbar/autosavemonate
2003-03-26coqide: locale iso-8859-1 par defaut si probleme. Interdiction des lemmes loc...monate
2003-03-14coqide: maj commandesmonate
2003-03-04IDE: majmonate
2003-02-24*** empty log message ***monate
2003-02-11Undo dans Coq IDEfilliatr
2003-02-04interface GTK2 experimentalemonate