aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEnrico Tassi2014-12-28 11:46:42 +0100
committerEnrico Tassi2014-12-28 11:46:42 +0100
commit5196c281298a3168b84f1df26b71f07c873f4b5d (patch)
tree2f291f2bc6876307024369e790f87c3d2b6ea4d6 /dev
parent0276f8357a2ea1d83cb6b85b86b8b3f5a1e4579d (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 'dev')
0 files changed, 0 insertions, 0 deletions