diff options
| author | Enrico Tassi | 2014-12-28 11:46:42 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-28 11:46:42 +0100 |
| commit | 5196c281298a3168b84f1df26b71f07c873f4b5d (patch) | |
| tree | 2f291f2bc6876307024369e790f87c3d2b6ea4d6 /plugins/syntax/string_syntax.ml | |
| parent | 0276f8357a2ea1d83cb6b85b86b8b3f5a1e4579d (diff) | |
Proof using: call "clear" to remove from sight the vars not selected
As discussed on coqdev, clear is not perfect, Hints for trivial
using cleared section vars are still used.
But it is better than nothing I guess.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions