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

3 files changed, 25 insertions, 11 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index dfe79a254..ec1e7415b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -703,7 +703,8 @@ GEXTEND Gram
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
       | IDENT "Implicit"; qid = global -> PrintImplicit qid
       | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
-      | IDENT "Assumptions"; qid = global -> PrintAssumptions qid ] ]
+      | IDENT "Assumptions"; qid = global -> PrintAssumptions (false, qid)
+      | IDENT "Opaque"; IDENT "Dependencies"; qid = global -> PrintAssumptions (true, qid) ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b86f5ce66..4eb8ae938 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -910,7 +910,8 @@ let rec pr_vernac = function
 	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
 (* spiwack: command printing all the axioms and section variables used in a 
          term *)
-	| PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
+	| PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
+	    ++spc()++pr_reference qid
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc -> 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index e2150fcbf..f26d4d9cf 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -498,10 +498,10 @@ let pr_assumptionset env s =
   if (Environ.ContextObjectMap.is_empty s) then
     str "Closed under the global context"
   else
-    let (vars,axioms) =
-      Environ.ContextObjectMap.fold (fun o typ r ->
-	let (v,a) = r in
-	match o with
+    let (vars,axioms,opaque) =
+      Environ.ContextObjectMap.fold (fun t typ r ->
+	let (v,a,o) = r in
+	match t with
 	| Variable id -> (  Some (
 	                      Option.default (fnl ()) v 
 			   ++ str (string_of_id id)
@@ -510,7 +510,7 @@ let pr_assumptionset env s =
 	                   ++ fnl ()
 			    )
 	                 ,
-	                   a )
+	                   a, o)
 	| Axiom kn    -> ( v ,
 			     Some (
 			      Option.default (fnl ()) a
@@ -519,16 +519,28 @@ let pr_assumptionset env s =
 	                   ++ pr_ltype typ
 	                   ++ fnl ()
 			     )
+			 , o
 			 )
-	)
-	s (None,None)
+	| Opaque kn    -> ( v , a ,
+			     Some (
+			      Option.default (fnl ()) o
+			   ++ (pr_constant env kn)
+	                   ++ str " : "
+	                   ++ pr_ltype typ
+	                   ++ fnl ()
+			     )
+			 )
+      )
+	s (None,None,None)
     in
-    let (vars,axioms) = 
+    let (vars,axioms,opaque) = 
       ( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
-	Option.map (fun p -> str "Axioms:" ++ p) axioms 
+	Option.map (fun p -> str "Axioms:" ++ p) axioms ,
+	Option.map (fun p -> str "Opaque constants:" ++ p) opaque
       )
     in
     (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
+      ++ (Option.default (mt ()) opaque)
 
 let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []