diff options
Diffstat (limited to 'library/assumptions.mli')
| -rw-r--r-- | library/assumptions.mli | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/library/assumptions.mli b/library/assumptions.mli index 0a2c62f5..bb36a972 100644 --- a/library/assumptions.mli +++ b/library/assumptions.mli @@ -9,6 +9,7 @@ open Util open Names open Term +open Globnames (** A few declarations for the "Print Assumption" command @author spiwack *) @@ -23,8 +24,18 @@ module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : Map.ExtS with type key = context_object and module Set := ContextObjectSet -(** collects all the assumptions (optionally including opaque definitions) - on which a term relies (together with their type) *) +(** Collects all the objects on which a term directly relies, bypassing kernel + opacity, together with the recursive dependence DAG of objects. + + WARNING: some terms may not make sense in the environment, because they are + sealed inside opaque modules. Do not try to do anything fancy with those + terms apart from printing them, otherwise demons may fly out of your nose. +*) +val traverse : constr -> (Refset.t * Refset.t Refmap.t) + +(** Collects all the assumptions (optionally including opaque definitions) + on which a term relies (together with their type). The above warning of + {!traverse} also applies. *) val assumptions : ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr -> Term.types ContextObjectMap.t |