From aa1022af5ec9970c8251d2bc3b074ae128e9e163 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 9 Mar 2009 19:47:26 +0000
Subject: 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
---
 toplevel/vernacentries.ml | 5 +++--
 toplevel/vernacexpr.ml    | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4e9edd90a4..b146e0c506 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1100,9 +1100,10 @@ let vernac_print = function
   | PrintAbout qid -> msgnl (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
 (*spiwack: prints all the axioms and section variables used by a term *)
-  | PrintAssumptions r ->
+  | PrintAssumptions (o,r) ->
       let cstr = constr_of_global (global_with_alias r) in
-      let nassumptions = Environ.assumptions cstr (Global.env ()) 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 global_module r =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 7a9e2b5a65..94ebce9ea7 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -65,7 +65,7 @@ type printable =
   | PrintVisibility of string option
   | PrintAbout of reference
   | PrintImplicit of reference
-  | PrintAssumptions of reference
+  | PrintAssumptions of bool * reference
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
-- 
cgit v1.2.3