diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-19 12:27:10 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-19 12:27:10 +0000 |
| commit | 54155675d0f5c724474d4bb6f16ca5f3fa60a6fe (patch) | |
| tree | 9b7c5de12314222e0ac08b3ffe010cf155d19af9 /lib/pp_control.mli | |
| parent | 49d8a6c11c2f0e6a7abb942980ebad3bcbb3456a (diff) | |
abstract+Defined: create opaque sub proofs (as pre-ParalITP)
Non-opaque-constant's side effects are processed before
the constant enters the kernel and global constants are
generated for them (as before, but not by side effect in
the middle of the proof construction).
This makes sense because proofs ending with Defined have
to be run immediately, so the list of side effects is
immediately available.
These side effects are type checked again.
To fix that the idea of kernel signatures could be employed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16702 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/pp_control.mli')
0 files changed, 0 insertions, 0 deletions