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 /kernel/declareops.ml | |
| 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 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index b0f320942..ac3aad15e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -226,7 +226,7 @@ let string_of_side_effect = function | NewConstant (c,_) -> Names.string_of_con c type side_effects = side_effect list let no_seff = ([] : side_effects) -let iter_side_effects f l = List.iter f l +let iter_side_effects f l = List.iter f (List.rev l) let fold_side_effects f a l = List.fold_left f a l let uniquize_side_effects l = List.uniquize l let union_side_effects l1 l2 = l1 @ l2 |