diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-06 08:21:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-06 08:21:03 +0000 |
| commit | 9953deaa45c642301a6cd7202b486c45923dece8 (patch) | |
| tree | 890acc9fddc816be6feeb8ce8f22a2f43e3382b8 /ide/coq.mli | |
| parent | efb0b098f13b816e5b38fbd16fd2b8cd85633b64 (diff) | |
- On adopte finalement la méthode de Pierre Courtieu pour le undo de
proof general (caractérisation des undos comme triplet d'un nombre de
Undo, n'un nombre de Abort et d'un Reset vers un état/id).
C'est plus simple et cela permet en plus d'avoir des buts imbriqués.
Au passage, "goto point" se comporte comme une suite de "one step back".
- Quelques bricoles sur la fenêtre préférences de Shortcuts.
- Quelques réorganisations autour du menu Display.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11058 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 930687eae..cec86ab78 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -35,7 +35,7 @@ type reset_mark = type reset_info = | NoReset | ResetAtSegmentStart of Names.identifier * bool ref - | ResetAtStatement of reset_mark * bool ref + | ResetAtStatement of bool ref | ResetAtRegisteredObject of reset_mark * bool ref val compute_reset_info : Vernacexpr.vernac_expr -> reset_info |