diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-24 14:32:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-24 14:32:25 +0000 |
| commit | 9fec60111a49960a01ffdd863d69fea57960edc5 (patch) | |
| tree | 607150b2a62cf6eb83167c1d0879811a79dd630a /library/lib.mli | |
| parent | ebf38f04cad3c4abbb779c3c40c1ba6d69bc0f71 (diff) | |
- Prise en compte des frozen state de Coq autant que possible pour
améliorer l'efficacité du undo. Restent les Qed et les End dont le
undo peut nécessiter de rejouer un segment arbitrairement complexe
(pour le undo du Qed, il faudrait typiquement que Coq se souvienne
de l'entrelacement de déclarations et de tactiques).
- Code mort concernant les mots-clés dans coq.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10982 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/library/lib.mli b/library/lib.mli index da8ace048..f3fa9a4b3 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -145,6 +145,9 @@ val reset_to : object_name -> unit val reset_name : identifier located -> unit val remove_name : identifier located -> unit val reset_mod : identifier located -> unit +val reset_to_state : object_name -> unit + +val has_top_frozen_state : unit -> object_name option (* [back n] resets to the place corresponding to the $n$-th call of [mark_end_of_command] (counting backwards) *) |