diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-11 11:18:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-11 11:18:41 +0000 |
| commit | ba61b1c136505c901c23f6a83cae6d29cedcd96c (patch) | |
| tree | 5fdf8bf7b8b678204291bd57f8413a1f5680ce6c /ide/coq.mli | |
| parent | f69af1fe44d2a1ff7260147ca643a4f4981379cd (diff) | |
Plutôt que de reposer sur le vernacexpr pour détecter les débuts de
buts, on se base sur les informations de Pfedit (comme le fait Pierre
Courtieu). Permet d'être plus robuste sur les extensions de syntaxe
ouvrant des buts, style Function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11101 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 9c95ec059..6208fba37 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -35,9 +35,12 @@ type reset_mark = type reset_status = | NoReset | ResetAtSegmentStart of Names.identifier - | ResetAtStatement of Libnames.object_name option | ResetAtRegisteredObject of reset_mark +type undo_info = int * int + +val undo_info : unit -> undo_info + type reset_info = reset_status * bool ref val compute_reset_info : Vernacexpr.vernac_expr -> reset_info |