diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 12:20:12 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 12:20:12 +0000 |
| commit | edcbdc62851c4ebef50ac8b2f67869f557e80242 (patch) | |
| tree | 47038bc43d6f385ea5fe8d16ef690fbe3b4255ee /kernel/declareops.ml | |
| parent | 6a5b186d2b53cf2c3e3a7ed5c238d26367a9df96 (diff) | |
ind_tables: properly handling side effects
If a constant is defined as transparent, not only its side effects
(opaque sub proofs as in abstract, and transparent ind schemes)
are declared globally, but the ones that are schemes are also declared
as such.
The only sub optimal thing is that the code handling in a special
way the side effects of transparent constants is in declare.ml that
does not see ind_tables.ml, hence a forward ref to a function is used.
IMO, ind_tables has no reason to stay in toplevel/.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16747 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 518a40a6e..9f981f482 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -254,7 +254,9 @@ let prune_constant_body cb = else {cb with const_constraints = cst'; const_body = cbo'} let string_of_side_effect = function - | NewConstant (c,_) -> Names.string_of_con c + | SEsubproof (c,_) -> Names.string_of_con c + | SEscheme (cl,_) -> + String.concat ", " (List.map (fun (_,c,_) -> Names.string_of_con c) cl) type side_effects = side_effect list let no_seff = ([] : side_effects) let iter_side_effects f l = List.iter f (List.rev l) |