diff options
| author | letouzey | 2012-07-11 16:50:17 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-11 16:50:17 +0000 |
| commit | 66483fbbb6549bc57bd409c689ee7d99e4d45d9d (patch) | |
| tree | 3e68c2f682ad5a55cd1c4a33b89fc954f4bbf99f /toplevel/backtrack.ml | |
| parent | df954f17d5f487e06ee21e10bab1ae9a133ba72d (diff) | |
Re-allow Reset in compiled files
This was a wish by A. Chlipala on coq-club
Both Reset foo and Reset Initial are accepted (with a warning).
If some proofs were opened, all of them are aborted. This isn't the
behavior of the interactive Reset that has more information and can
be more selective, but this shouldn't be a big issue in practice.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15597 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/backtrack.ml')
| -rw-r--r-- | toplevel/backtrack.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index d0f258fbf8..fb25be7c11 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -40,6 +40,11 @@ type info = { let history : info Stack.t = Stack.create () +(** Is this stack active (i.e. nonempty) ? + The stack is currently inactive when compiling files (coqc). *) + +let is_active () = not (Stack.is_empty history) + (** For debug purpose, a dump of the history *) let dump_history () = |