Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

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