Documenting the caveat of assumption printing in the mli.

1 files changed, 10 insertions, 4 deletions

diff --git a/library/assumptions.mli b/library/assumptions.mli
index 78d2806497..809e536b43 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -24,12 +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 objects on which a term directly relies, bypassing kernel
-    opacity, together with the recursive dependence DAG of objects *)
+(** 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 environement, 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) *)
+(** 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