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/environ.mli | |
| 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/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index b0dc2846f9..9e1afdf19b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -244,13 +244,14 @@ val register : env -> field -> Retroknowledge.entry -> env type context_object = | Variable of identifier (* A section variable or a Let definition *) | Axiom of constant (* An axiom or a constant. *) + | Opaque of constant (* An opaque constant. *) (* AssumptionSet.t is a set of [assumption] *) module OrderedContextObject : Set.OrderedType with type t = context_object module ContextObjectMap : Map.S with type key = context_object -(* collects all the assumptions on which a term relies (together with - their type *) -val assumptions : constr -> env -> Term.types ContextObjectMap.t +(* collects all the assumptions (optionally including opaque definitions) + on which a term relies (together with their type) *) +val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t |