First attempt at making Print Assumption compatible with opaque modules (fix #2168)

 We replace Global.lookup_constant by our own code that looks for a module
 and enters its implementation. This is still preliminary work, I would prefer
 to understand more completely the part about module substitutions when
 entering an applied functor. But this code already appears to work quite well.
 Anyway, since we only search for constants, we don't need to reconstitute a
 100% accurate environment, as long as the same objects are in it.

 Note:

  - Digging inside module structures is slower than just using
    Global.lookup_constant. Hence we try to avoid it as long as we could.
    Only in front of axioms (or in front of constant unknown to Global)
    do we check whether we have an inner-module implementation for this
    constant. There is some memoization of the search for internal
    structure_body out of a module_path.

  - In case of inner-module axioms, we might not be able to print
    its type, but only its long name.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 410 insertions, 192 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index b88e4ebca..4df8b9cc4 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -66,6 +66,7 @@ Lib
 Goptions
 Decls
 Heads
+Assumptions
 Termops
 Namegen
 Evd
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a0b7d2cbc..59336a762 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -528,144 +528,3 @@ fun env field value ->
   in
   Retroknowledge.add_field retroknowledge_with_reactive_info field value
   }
-
-
-(**************************************************************)
-(* spiwack: the following definitions are used by the function
-   [assumptions] which gives as an output the set of all
-   axioms and sections variables on which a given term depends
-   in a context (expectingly the Global context) *)
-
-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. *)
-
-(* Defines a set of [assumption] *)
-module OrderedContextObject =
-struct
-  type t = context_object
-  let compare x y =
-      match x , y with
-      | Variable i1 , Variable i2 -> id_ord i1 i2
-      | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2
-	          (* spiwack: it would probably be cleaner
-		     to provide a [kn_ord] function *)
-      | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2
-      | Variable _ , Axiom _ -> -1
-      | Axiom _ , Variable _ -> 1
-      | Opaque _ , _ -> -1
-      | _, Opaque _ -> 1
-end
-
-module ContextObjectSet = Set.Make (OrderedContextObject)
-module ContextObjectMap = Map.Make (OrderedContextObject)
-
-
-let assumptions ?(add_opaque=false) st (* t env *) =
-  let (idts,knst) = st in
-  (* Infix definition for chaining function that accumulate
-     on a and a ContextObjectSet, ContextObjectMap.  *)
-  let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
-  (* This function eases memoization, by checking if an object is already
-     stored before trying and applying a function.
-     If the object is there, the function is not fired (we are in a
-     particular case where memoized object don't need a treatment at all).
-     If the object isn't there, it is stored and the function is fired*)
-  let try_and_go o f s m =
-    if ContextObjectSet.mem o s then
-      (s,m)
-    else
-      f (ContextObjectSet.add o s) m
-  in
-  let identity2 s m = (s,m) in
-  (* Goes recursively into the term to see if it depends on assumptions
-    the 3 important cases are : - Const _ where we need to first unfold
-    the constant and return the needed assumptions of its body in the
-    environment,
-                                - Rel _ which means the term is a variable
-    which has been bound earlier by a Lambda or a Prod (returns [] ),
-                                - Var _ which means that the term refers
-    to a section variable or a "Let" definition, in the former it is
-    an assumption of [t], in the latter is must be unfolded like a Const.
-    The other cases are straightforward recursion.
-    Calls to the environment are memoized, thus avoiding to explore
-    the DAG of the environment as if it was a tree (can cause
-    exponential behavior and prevent the algorithm from terminating
-    in reasonable time). [s] is a set of [context_object], representing
-    the object already visited.*)
-  let rec aux t env s acc =
-    match kind_of_term t with
-    | Var id -> aux_memoize_id id env s acc
-    | Meta _ | Evar _ ->
-	Util.anomaly "Environ.assumption: does not expect a meta or an evar"
-    | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) ->
-                           ((aux e1 env)**(aux e2 env)) s acc
-    | LetIn (_,e1,e2,e3) -> ((aux e1 env)**
-                             (aux e2 env)**
-                             (aux e3 env))
-	                     s acc
-    | App (e1, e_array) -> ((aux e1 env)**
-			    (Array.fold_right
-			       (fun e f -> (aux e env)**f)
-                               e_array identity2))
-	                   s acc
-    | Case (_,e1,e2,e_array) -> ((aux e1 env)**
-                                 (aux e2 env)**
-				 (Array.fold_right
-				    (fun e f -> (aux e env)**f)
-                                    e_array identity2))
-	                        s acc
-    | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
-                  ((Array.fold_right
-		      (fun e f -> (aux e env)**f)
-                      e1_array identity2) **
-                   (Array.fold_right
-		      (fun e f -> (aux e env)**f)
-                      e2_array identity2))
-		     s acc
-    | Const kn -> aux_memoize_kn kn env s acc
-    | _ -> (s,acc) (* closed atomic types + rel *)
-
-  and add_id id env s acc =
-    (* a Var can be either a variable, or a "Let" definition.*)
-    match lookup_named id env with
-    | (_,None,t) ->
-        (s,ContextObjectMap.add (Variable id) t acc)
-    | (_,Some bdy,_) -> aux bdy env s acc
-
-  and aux_memoize_id id env =
-    try_and_go (Variable id) (add_id id env)
-
-  and add_kn kn env s acc =
-    let cb = lookup_constant kn env in
-    let do_type cst =
-      let ctype =
-	match cb.Declarations.const_type with
-	| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
-	| NonPolymorphicType t -> t
-      in
-	(s,ContextObjectMap.add cst ctype acc)
-    in
-    let (s,acc) =
-      if Declarations.constant_has_body cb
-	&& (Declarations.is_opaque cb || not (Cpred.mem kn knst))
-	&& add_opaque
-      then
-	do_type (Opaque kn)
-      else (s,acc)
-    in
-      match Declarations.body_of_constant cb with
-      | None -> do_type (Axiom kn)
-      | Some body -> aux (Declarations.force body) env s acc
-
-  and aux_memoize_kn kn env =
-    try_and_go (Axiom kn) (add_kn kn env)
- in
- fun t env ->
-   snd (aux t env (ContextObjectSet.empty) (ContextObjectMap.empty))
-
-(* /spiwack *)
-
-
-
diff --git a/kernel/environ.mli b/kernel/environ.mli
index af1e17591..aa6f52128 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -228,20 +228,3 @@ val unregister : env -> field -> env
 val register : env -> field -> Retroknowledge.entry -> env
 
 
-
-(** a few declarations for the "Print Assumption" command 
-    @author spiwack *)
-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 (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
-
-
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index a628e5cfe..8c1dd53ad 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -29,4 +29,4 @@ Safe_typing
 
 Vm
 Csymtable
-Vconv
\ No newline at end of file
+Vconv
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e4cb78bde..c620d8dd2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -197,22 +197,6 @@ let update_resolver f senv =
   { senv with modinfo = { mi with resolver = f mi.resolver }}
 
 
-(*spiwack: functions for safe retroknowledge *)
-
-(* 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 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
-   include at least all the closed terms. But it could contain other ones
-   like the axiom of excluded middle for instance *)
-let safe =
-  closed
-
-
-
 (* universal lifting, used for the "get" operations mostly *)
 let retroknowledge f senv =
   Environ.retroknowledge f (env_of_senv senv)
diff --git a/library/assumptions.ml b/library/assumptions.ml
new file mode 100644
index 000000000..adc7f8edc
--- /dev/null
+++ b/library/assumptions.ml
@@ -0,0 +1,238 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* The following definitions are used by the function
+   [assumptions] which gives as an output the set of all
+   axioms and sections variables on which a given term depends
+   in a context (expectingly the Global context) *)
+
+(* Initial author: Arnaud Spiwack
+   Module-traversing code: Pierre Letouzey *)
+
+open Util
+open Names
+open Sign
+open Univ
+open Term
+open Declarations
+open Mod_subst
+
+let cst_ord k1 k2 = kn_ord (canonical_con k1) (canonical_con k2)
+
+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. *)
+
+(* Defines a set of [assumption] *)
+module OrderedContextObject =
+struct
+  type t = context_object
+  let compare x y =
+      match x , y with
+      | Variable i1 , Variable i2 -> id_ord i1 i2
+      | Axiom k1 , Axiom k2 -> cst_ord k1 k2
+      | Opaque k1 , Opaque k2 -> cst_ord k1 k2
+      | Variable _ , Axiom _ -> -1
+      | Axiom _ , Variable _ -> 1
+      | Opaque _ , _ -> -1
+      | _, Opaque _ -> 1
+end
+
+module ContextObjectSet = Set.Make (OrderedContextObject)
+module ContextObjectMap = Map.Make (OrderedContextObject)
+
+(** For a constant c in a module sealed by an interface (M:T and
+    not M<:T), [Global.lookup_constant] may return a [constant_body]
+    without body. We fix this by looking in the implementation
+    of the module *)
+
+let modcache = ref (MPmap.empty : structure_body MPmap.t)
+
+let rec lookup_module_in_impl mp =
+  try Global.lookup_module mp
+  with Not_found ->
+    (* The module we search might not be exported by its englobing module(s).
+       We access the upper layer, and then do a manual search *)
+    match mp with
+      | MPfile _ | MPbound _ ->
+	raise Not_found (* should have been found by [lookup_module] *)
+      | MPdot (mp',lab') ->
+	let fields = memoize_fields_of_mp mp' in
+	match List.assoc lab' fields with
+	  | SFBmodule mb -> mb
+	  | _ -> assert false (* same label for a non-module ?! *)
+
+and memoize_fields_of_mp mp =
+  try MPmap.find mp !modcache
+  with Not_found ->
+    let l = fields_of_mp mp in
+    modcache := MPmap.add mp l !modcache;
+    l
+
+and fields_of_mp mp =
+  let mb = lookup_module_in_impl mp in
+  let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in
+  let subs =
+    if inner_mp = mp then subs
+    else add_mp inner_mp mp mb.mod_delta subs
+  in
+  Modops.subst_signature subs fields
+
+and fields_of_mb subs mb args =
+  let seb = match mb.mod_expr with
+    | None -> mb.mod_type (* cf. Declare Module *)
+    | Some seb -> seb
+  in
+  fields_of_seb subs mb.mod_mp seb args
+
+(* TODO: using [empty_delta_resolver] below in [fields_of_seb]
+   is probably slightly incorrect. But:
+    a) I don't see currently what should be used instead
+    b) this shouldn't be critical for Print Assumption. At worse some
+       constants will have a canonical name which is non-canonical,
+       leading to failures in [Global.lookup_constant], but our own
+       [lookup_constant] should work.
+*)
+
+and fields_of_seb subs mp0 seb args = match seb with
+  | SEBstruct l ->
+    assert (args = []);
+    l, mp0, subs
+  | SEBident mp ->
+    let mb = lookup_module_in_impl (subst_mp subs mp) in
+    fields_of_mb subs mb args
+  | SEBapply (seb1,seb2,_) ->
+    (match seb2 with
+      | SEBident mp2 -> fields_of_seb subs mp0 seb1 (mp2::args)
+      | _ -> assert false) (* only legal application is to module names *)
+  | SEBfunctor (mbid,mtb,seb) ->
+    (match args with
+      | [] -> assert false (* we should only encounter applied functors *)
+      | mpa :: args ->
+	let subs = add_mbid mbid mpa empty_delta_resolver subs in
+	fields_of_seb subs mp0 seb args)
+  | SEBwith _ -> assert false (* should not appear in a mod_expr
+				   or mod_type field *)
+
+let lookup_constant_in_impl cst fallback =
+  try
+    let mp,dp,lab = repr_kn (canonical_con cst) in
+    let fields = memoize_fields_of_mp mp in
+    (* A module found this way is necessarily closed, in particular
+       our constant cannot be in an opened section : *)
+    match List.assoc lab fields with
+      | SFBconst cb -> cb
+      | _ -> assert false (* label not pointing to a constant ?! *)
+  with Not_found ->
+    (* Either:
+       - The module part of the constant isn't registered yet :
+         we're still in it, so the [constant_body] found earlier
+         (if any) was a true axiom.
+       - The label has not been found in the structure. This is an error *)
+    match fallback with
+      | Some cb -> cb
+      | None -> anomaly ("Print Assumption: unknown constant "^string_of_con cst)
+
+let lookup_constant cst =
+  try
+    let cb = Global.lookup_constant cst in
+    if constant_has_body cb then cb
+    else lookup_constant_in_impl cst (Some cb)
+  with Not_found -> lookup_constant_in_impl cst None
+
+let assumptions ?(add_opaque=false) st (* t *) =
+  modcache := MPmap.empty;
+  let (idts,knst) = st in
+  (* Infix definition for chaining function that accumulate
+     on a and a ContextObjectSet, ContextObjectMap.  *)
+  let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
+  (* This function eases memoization, by checking if an object is already
+     stored before trying and applying a function.
+     If the object is there, the function is not fired (we are in a
+     particular case where memoized object don't need a treatment at all).
+     If the object isn't there, it is stored and the function is fired*)
+  let try_and_go o f s m =
+    if ContextObjectSet.mem o s then
+      (s,m)
+    else
+      f (ContextObjectSet.add o s) m
+  in
+  let identity2 s m = (s,m)
+  in
+  (* Goes recursively into the term to see if it depends on assumptions.
+    The 3 important cases are :
+     - Const _ where we need to first unfold the constant and return
+       the needed assumptions of its body in the environment,
+     - Rel _ which means the term is a variable which has been bound
+       earlier by a Lambda or a Prod (returns [] ),
+     - Var _ which means that the term refers to a section variable or
+       a "Let" definition, in the former it is an assumption of [t],
+       in the latter is must be unfolded like a Const.
+    The other cases are straightforward recursion.
+    Calls to the environment are memoized, thus avoiding to explore
+    the DAG of the environment as if it was a tree (can cause
+    exponential behavior and prevent the algorithm from terminating
+    in reasonable time). [s] is a set of [context_object], representing
+    the object already visited.*)
+  let rec do_constr t s acc =
+    let rec iter t =
+      match kind_of_term t with
+	| Var id -> do_memoize_id id
+	| Meta _ | Evar _ -> assert false
+	| Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) ->
+	  (iter e1)**(iter e2)
+	| LetIn (_,e1,e2,e3) -> (iter e1)**(iter e2)**(iter e3)
+	| App (e1, e_array) -> (iter e1)**(iter_array e_array)
+	| Case (_,e1,e2,e_array) -> (iter e1)**(iter e2)**(iter_array e_array)
+	| Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
+          (iter_array e1_array) ** (iter_array e2_array)
+	| Const kn -> do_memoize_kn kn
+	| _ -> identity2 (* closed atomic types + rel *)
+    and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2
+    in iter t s acc
+
+  and add_id id s acc =
+    (* a Var can be either a variable, or a "Let" definition.*)
+    match Global.lookup_named id with
+    | (_,None,t) ->
+        (s,ContextObjectMap.add (Variable id) t acc)
+    | (_,Some bdy,_) -> do_constr bdy s acc
+
+  and do_memoize_id id =
+    try_and_go (Variable id) (add_id id)
+
+  and add_kn kn s acc =
+    let cb = lookup_constant kn in
+    let do_type cst =
+      let ctype =
+	match cb.Declarations.const_type with
+	| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+	| NonPolymorphicType t -> t
+      in
+	(s,ContextObjectMap.add cst ctype acc)
+    in
+    let (s,acc) =
+      if add_opaque && Declarations.constant_has_body cb
+	&& (Declarations.is_opaque cb || not (Cpred.mem kn knst))
+      then
+	do_type (Opaque kn)
+      else (s,acc)
+    in
+      match Declarations.body_of_constant cb with
+      | None -> do_type (Axiom kn)
+      | Some body -> do_constr (Declarations.force body) s acc
+
+  and do_memoize_kn kn =
+    try_and_go (Axiom kn) (add_kn kn)
+
+ in
+ fun t ->
+   snd (do_constr t
+	  (ContextObjectSet.empty)
+	  (ContextObjectMap.empty))
diff --git a/library/assumptions.mli b/library/assumptions.mli
new file mode 100644
index 000000000..1e3e9ef86
--- /dev/null
+++ b/library/assumptions.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Term
+open Environ
+
+(** A few declarations for the "Print Assumption" command
+    @author spiwack *)
+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 (optionally including opaque definitions)
+   on which a term relies (together with their type) *)
+val assumptions :
+  ?add_opaque:bool -> transparent_state -> constr ->
+    Term.types ContextObjectMap.t
diff --git a/library/library.mllib b/library/library.mllib
index 4efb69a21..e8b5a7a4c 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -13,4 +13,4 @@ Dischargedhypsmap
 Goptions
 Decls
 Heads
-
+Assumptions
\ No newline at end of file
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 232551984..404e1b6ae 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -489,14 +489,26 @@ let pr_prim_rule = function
 let prterm = pr_lconstr
 
 
-(* spiwack: printer function for sets of Environ.assumption.
-            It is used primarily by the Print Assumption command. *)
+(* Printer function for sets of Assumptions.assumptions.
+   It is used primarily by the Print Assumptions command. *)
+
+open Assumptions
+
 let pr_assumptionset env s =
-  if (Environ.ContextObjectMap.is_empty s) then
-    str "Closed under the global context"
+  if ContextObjectMap.is_empty s then
+    str "Closed under the global context" ++ fnl()
   else
+    let safe_pr_constant env kn =
+      try pr_constant env kn
+      with Not_found ->
+	let mp,_,lab = repr_con kn in
+	str (string_of_mp mp ^ "." ^ string_of_label lab)
+    in
+    let safe_pr_ltype typ =
+      try str " : " ++ pr_ltype typ with _ -> mt ()
+    in
     let (vars,axioms,opaque) =
-      Environ.ContextObjectMap.fold (fun t typ r ->
+      ContextObjectMap.fold (fun t typ r ->
 	let (v,a,o) = r in
 	match t with
 	| Variable id -> (  Some (
@@ -511,9 +523,8 @@ let pr_assumptionset env s =
 	| Axiom kn    -> ( v ,
 			     Some (
 			      Option.default (fnl ()) a
-			   ++ (pr_constant env kn)
-	                   ++ str " : "
-	                   ++ pr_ltype typ
+			   ++ safe_pr_constant env kn
+	                   ++ safe_pr_ltype typ
 	                   ++ fnl ()
 			     )
 			 , o
@@ -521,9 +532,8 @@ let pr_assumptionset env s =
 	| Opaque kn    -> ( v , a ,
 			     Some (
 			      Option.default (fnl ()) o
-			   ++ (pr_constant env kn)
-	                   ++ str " : "
-	                   ++ pr_ltype typ
+			   ++ safe_pr_constant env kn
+	                   ++ safe_pr_ltype typ
 	                   ++ fnl ()
 			     )
 			 )
diff --git a/parsing/printer.mli b/parsing/printer.mli
index b7e581cd5..7e08d80fc 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -134,7 +134,8 @@ val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 
 (** spiwack: printer function for sets of Environ.assumption.
             It is used primarily by the Print Assumption command. *)
-val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds
+val pr_assumptionset :
+  env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds
 
 val pr_goal_by_id : string -> std_ppcmds
 
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
new file mode 100644
index 000000000..23f33081b
--- /dev/null
+++ b/test-suite/output/PrintAssumptions.out
@@ -0,0 +1,18 @@
+Axioms:
+foo : nat
+Axioms:
+foo : nat
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Closed under the global context
+Closed under the global context
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
new file mode 100644
index 000000000..f23bc4980
--- /dev/null
+++ b/test-suite/output/PrintAssumptions.v
@@ -0,0 +1,96 @@
+
+(** Print Assumption and opaque modules :
+
+  Print Assumption used to consider as axioms the modular fields
+  unexported by their signature, cf bug report #2186. This should
+  now be fixed, let's test this here. *)
+
+(* First, a minimal test-case *)
+
+Axiom foo : nat.
+
+Module Type T.
+ Parameter bar : nat.
+End T.
+
+Module M : T.
+  Module Hide. (* An entire sub-module could be hidden *)
+  Definition x := foo.
+  End Hide.
+  Definition bar := Hide.x.
+End M.
+
+Module N (X:T) : T.
+  Definition y := X.bar. (* A non-exported field *)
+  Definition bar := y.
+End N.
+
+Module P := N M.
+
+Print Assumptions M.bar. (* Should answer: foo *)
+Print Assumptions P.bar. (* Should answer: foo *)
+
+
+(* The original test-case of the bug-report *)
+
+Require Import Arith.
+
+Axiom extensionality : forall P Q (f g:P -> Q),
+  (forall x, f x = g x) -> f = g.
+
+Module Type ADD_COMM_EXT.
+  Axiom add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+End ADD_COMM_EXT.
+
+Module AddCommExt_Opaque : ADD_COMM_EXT.
+  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+  Proof.
+    intro n; apply extensionality; auto with arith.
+  Qed.
+End AddCommExt_Opaque.
+
+Module AddCommExt_Transparent <: ADD_COMM_EXT.
+  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+  Proof.
+    intro n; apply extensionality; auto with arith.
+  Qed.
+End AddCommExt_Transparent.
+
+Print Assumptions AddCommExt_Opaque.add_comm_ext.
+(* Should answer: extensionality *)
+
+Print Assumptions AddCommExt_Transparent.add_comm_ext.
+(* Should answer: extensionality *)
+
+Lemma add1_comm_ext_opaque :
+  (fun x => x + 1) = (fun x => 1 + x).
+Proof (AddCommExt_Opaque.add_comm_ext 1).
+
+Lemma add1_comm_ext_transparent :
+  (fun x => x + 1) = (fun x => 1 + x).
+Proof (AddCommExt_Transparent.add_comm_ext 1).
+
+Print Assumptions add1_comm_ext_opaque.
+(* Should answer: extensionality *)
+
+Print Assumptions add1_comm_ext_transparent.
+(* Should answer: extensionality *)
+
+Module Type FALSE_POSITIVE.
+  Axiom add_comm : forall n x, x + n = n + x.
+End FALSE_POSITIVE.
+
+Module false_positive : FALSE_POSITIVE.
+  Lemma add_comm : forall n x, x + n = n + x.
+  Proof. auto with arith. Qed.
+
+  Print Assumptions add_comm.
+  (* Should answer : Closed under the global context *)
+End false_positive.
+
+Lemma comm_plus5 : forall x,
+  x + 5 = 5 + x.
+Proof (false_positive.add_comm 5).
+
+Print Assumptions comm_plus5.
+(* Should answer : Closed under the global context *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2def852aa..0de85a456 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1110,12 +1110,12 @@ let vernac_print = function
       pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintAbout qid -> msg (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
-(*spiwack: prints all the axioms and section variables used by a term *)
   | PrintAssumptions (o,r) ->
+      (* Prints all the axioms and section variables used by a term *)
       let cstr = constr_of_global (smart_global r) in
-      let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ())
-	~add_opaque:o cstr (Global.env ()) in
-      msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
+      let st = Conv_oracle.get_transp_state () in
+      let nassums = Assumptions.assumptions st ~add_opaque:o cstr in
+      msg (Printer.pr_assumptionset (Global.env ()) nassums)
 
 let global_module r =
   let (loc,qid) = qualid_of_reference r in