diff options
| author | msozeau | 2009-03-09 19:47:26 +0000 |
|---|---|---|
| committer | msozeau | 2009-03-09 19:47:26 +0000 |
| commit | aa1022af5ec9970c8251d2bc3b074ae128e9e163 (patch) | |
| tree | 31fd3e1436a5b1f8c53dc9f4427b4fd4f89b3497 /kernel/safe_typing.ml | |
| parent | c33e70150a45d9d8052548e2b3f57d8bc6f28ecb (diff) | |
Optionally list opaque constants in addition to axions/variables in
assumptions. Feel free to rename "Print Opaque Dependencies" to
something better.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 09b2f918f0..7469e12181 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -114,7 +114,7 @@ let add_constraints cst senv = (* terms which are closed under the environnement env, i.e terms which only depends on constant who are themselves closed *) let closed env term = - ContextObjectMap.is_empty (assumptions env term) + ContextObjectMap.is_empty (assumptions full_transparent_state env term) (* the set of safe terms in an environement any recursive set of terms who are known not to prove inconsistent statement. It should |