index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
ide
/
coq.mli
Age
Commit message (
Expand
)
Author
2010-02-26
New backtracking code + fix bug #2082.
vgross
2010-02-26
Introducing a dual stack setup
vgross
2010-02-26
New API for backtracking.
vgross
2010-02-26
Redispatch of printing tweaking hooks.
vgross
2010-02-12
Simplify backtracking
vgross
2010-02-12
Refactoring of the printing options
vgross
2010-01-11
Revert "Isolation of proof-displaying code"
vgross
2010-01-11
Isolation of proof-displaying code
vgross
2009-12-11
Deport the backtracking code out of the ide
vgross
2009-12-03
Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1
vgross
2009-11-19
Refactoring of coqide backtrack code, with the intent to put everything
vgross
2009-10-05
Revert "kills the old backtracking framework and replaces it with"
vgross
2009-09-29
kills the old backtracking framework and replaces it with
vgross
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-06-22
clearing unused functions
vgross
2009-06-11
Simplifying the call to print_no_goals and not calling it when no goal
herbelin
2009-06-07
Partial simplification of undo mechanism, relying only on Courtieu's
herbelin
2009-05-27
keeping interface synch'ed
vgross
2008-06-13
CoqIDE: 2 problèmes de undo encore:
herbelin
2008-06-11
Plutôt que de reposer sur le vernacexpr pour détecter les débuts de
herbelin
2008-06-09
On prend des risques en tentant d'optimiser encore plus le undo en cas
herbelin
2008-06-06
- On adopte finalement la méthode de Pierre Courtieu pour le undo de
herbelin
2008-05-28
Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image de
herbelin
2008-05-26
Réorganisation des points d'appui du undo de CoqIDE (type reset_info).
herbelin
2008-05-25
- Nouvelle option "Set Printing Existential Instances" pour forcer
herbelin
2008-05-24
- Prise en compte des frozen state de Coq autant que possible pour
herbelin
2008-05-10
Amélioration de la colorisation, du backtrack et des messages de CoqIDE
herbelin
2008-05-08
** Efficacité, bugs, robustesse CoqIDE **
herbelin
2007-04-26
fin des conclusions multiples
corbinea
2006-09-20
Declarative Proof Language: main commit
corbinea
2006-05-30
Correction bug #990 (LoadPath et option -R de coqide
notin
2005-01-21
Compatibilité ocamlweb pour cible doc
herbelin
2004-07-18
Abstraction vis a vis du type loc pour ocaml 3.08
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2004-03-03
ide: silent behavior better, save icon, -byte works
marche
2003-09-19
Coqide : les nouveaute d'aout
monate
2003-07-16
coqide: fixed problems with -R -I and coqide interaction
monate
2003-06-25
coqide : status bar more informative, forbid Section/Module in proo mode
monate
2003-06-13
CoqIDE: undo immediat sur les commandes ne modifiant pas l'etat
filliatr
2003-05-26
coqide: blaster interruptible
monate
2003-05-22
coqide: blaster V1
monate
2003-05-07
coqide: toolbar/autosave
monate
2003-03-26
coqide: locale iso-8859-1 par defaut si probleme. Interdiction des lemmes loc...
monate
2003-03-14
coqide: maj commandes
monate
2003-03-04
IDE: maj
monate
2003-02-24
*** empty log message ***
monate
2003-02-11
Undo dans Coq IDE
filliatr
2003-02-04
interface GTK2 experimentale
monate