diff options
| author | bertot | 2001-02-13 07:40:31 +0000 |
|---|---|---|
| committer | bertot | 2001-02-13 07:40:31 +0000 |
| commit | fc507c51aba9e0258e41e3ea4c8b38bf2cc0dc1b (patch) | |
| tree | 24c129848fc7a79255467bae9b1d16c1548f6f0f /kernel/type_errors.ml | |
| parent | a9662447f937057a9411ee5e6a6ba74fda93f989 (diff) | |
Make sure the initial state used in a protected loop is the state chose exactly
at the time the protected loop was started. This makes it possible
to have modifications of commands specific to the protected loop remembered
throughout the session.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1371 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions