Fixed #2926:

Extend "Print Opaque Dependencies" for transparent dependencies as
well

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

7 files changed, 97 insertions, 65 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 25897950e3..97080fdad5 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -65,7 +65,7 @@ type printable =
   | PrintVisibility of string option
   | PrintAbout of reference or_by_notation
   | PrintImplicit of reference or_by_notation
-  | PrintAssumptions of bool * reference or_by_notation
+  | PrintAssumptions of bool * bool * reference or_by_notation
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
diff --git a/library/assumptions.ml b/library/assumptions.ml
index d721311e06..bd1292e7ac 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -27,6 +27,7 @@ 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. *)
+  | Transparent of constant
 
 (* Defines a set of [assumption] *)
 module OrderedContextObject =
@@ -37,10 +38,14 @@ struct
       | 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
+      | Transparent k1 , Transparent k2 -> cst_ord k1 k2
       | Axiom _ , Variable _ -> 1
-      | Opaque _ , _ -> -1
-      | _, Opaque _ -> 1
+      | Opaque _ , Variable _
+      | Opaque _ , Axiom _ -> 1
+      | Transparent _ , Variable _
+      | Transparent _ , Axiom _
+      | Transparent _ , Opaque _ -> 1
+      | _ , _ -> -1
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)
@@ -151,7 +156,7 @@ let lookup_constant cst =
     else lookup_constant_in_impl cst (Some cb)
   with Not_found -> lookup_constant_in_impl cst None
 
-let assumptions ?(add_opaque=false) st (* t *) =
+let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
   modcache := MPmap.empty;
   let (idts,knst) = st in
   (* Infix definition for chaining function that accumulate
@@ -223,11 +228,15 @@ let assumptions ?(add_opaque=false) st (* t *) =
 	(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)
+      if Declarations.constant_has_body cb then
+        if Declarations.is_opaque cb || not (Cpred.mem kn knst) then
+          (** it is opaque *)
+          if add_opaque then do_type (Opaque kn)
+          else (s, acc)
+        else
+          if add_transparent then do_type (Transparent kn)
+          else (s, acc)
+      else (s, acc)
     in
       match Declarations.body_of_constant cb with
       | None -> do_type (Axiom kn)
diff --git a/library/assumptions.mli b/library/assumptions.mli
index 5d16ac7253..e5d2a977cb 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -13,9 +13,10 @@ 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. *)
+  | Variable of identifier  (** A section variable or a Let definition *)
+  | Axiom of constant       (** An axiom or a constant. *)
+  | Opaque of constant      (** An opaque constant. *)
+  | Transparent of constant (** A transparent constant *)
 
 (** AssumptionSet.t is a set of [assumption] *)
 module OrderedContextObject :  Set.OrderedType with type t = context_object
@@ -24,5 +25,5 @@ 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 ->
+  ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr ->
     Term.types ContextObjectMap.t
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0519bee8cb..40eb78cdcc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -862,8 +862,11 @@ GEXTEND Gram
       | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid
       | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (false, fopt)
       | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (true, fopt)
-      | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, qid)
-      | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, qid) ] ]
+      | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, false, qid)
+      | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, false, qid)
+      | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (false, true, qid)
+      | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, true, qid) ] ]
+
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index b914e38775..8d763c2d1f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -430,6 +430,58 @@ let pr_record_decl b c fs =
     hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
 in
 
+let pr_printable = function
+| PrintFullContext -> str "Print All"
+| PrintSectionContext s ->
+    str "Print Section" ++ spc() ++ Libnames.pr_reference s
+| PrintGrammar ent ->
+    str "Print Grammar" ++ spc() ++ str ent
+| PrintLoadPath dir -> str "Print LoadPath" ++ pr_opt pr_dirpath dir
+| PrintModules -> str "Print Modules"
+| PrintMLLoadPath -> str "Print ML Path"
+| PrintMLModules -> str "Print ML Modules"
+| PrintGraph -> str "Print Graph"
+| PrintClasses -> str "Print Classes"
+| PrintTypeClasses -> str "Print TypeClasses"
+| PrintInstances qid -> str "Print Instances" ++ spc () ++ pr_smart_global qid
+| PrintLtac qid -> str "Print Ltac" ++ spc() ++ pr_ltac_ref qid
+| PrintCoercions -> str "Print Coercions"
+| PrintCoercionPaths (s,t) -> str "Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
+| PrintCanonicalConversions -> str "Print Canonical Structures"
+| PrintTables -> str "Print Tables"
+| PrintHintGoal -> str "Print Hint"
+| PrintHint qid -> str "Print Hint" ++ spc() ++ pr_smart_global qid
+| PrintHintDb -> str "Print Hint *"
+| PrintHintDbName s -> str "Print HintDb" ++ spc() ++ str s
+| PrintRewriteHintDbName s -> str "Print Rewrite HintDb" ++ spc() ++ str s
+| PrintUniverses (b, fopt) ->
+  let cmd =
+    if b then "Print Sorted Universes"
+    else "Print Universes"
+  in
+  str cmd ++ pr_opt str fopt
+| PrintName qid -> str "Print" ++ spc()  ++ pr_smart_global qid
+| PrintModuleType qid -> str "Print Module Type" ++ spc() ++ pr_reference qid
+| PrintModule qid -> str "Print Module" ++ spc() ++ pr_reference qid
+| PrintInspect n -> str "Inspect" ++ spc() ++ int n
+| PrintScopes -> str "Print Scopes"
+| PrintScope s -> str "Print Scope" ++ spc() ++ str s
+| PrintVisibility s -> str "Print Visibility" ++ pr_opt str s
+| PrintAbout qid -> str "About" ++ spc()  ++ pr_smart_global qid
+| PrintImplicit qid -> str "Print Implicit" ++ spc()  ++ pr_smart_global qid
+(* spiwack: command printing all the axioms and section variables used in a
+  term *)
+| PrintAssumptions (b, t, qid) ->
+  let cmd = match b, t with
+  | true, true -> "Print All Dependencies"
+  | true, false -> "Print Opaque Dependencies"
+  | false, true -> "Print Transparent Dependencies"
+  | false, false -> "Print Assumptions"
+  in
+  str cmd ++ spc() ++ pr_smart_global qid
+| PrintNamespace dp -> str "Print Namespace" ++ pr_dirpath dp
+in
+
 let rec pr_vernac = function
 
   (* Proof management *)
@@ -860,47 +912,7 @@ let rec pr_vernac = function
   | VernacDeclareReduction (b,s,r) ->
      pr_locality b ++ str "Declare Reduction " ++ str s ++ str " := " ++
      pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
-  | VernacPrint p ->
-      let pr_printable = function
-	| PrintFullContext -> str"Print All"
-	| PrintSectionContext s ->
-            str"Print Section" ++ spc() ++ Libnames.pr_reference s
-	| PrintGrammar ent ->
-            str"Print Grammar" ++ spc() ++ str ent
-	| PrintLoadPath dir -> str"Print LoadPath" ++ pr_opt pr_dirpath dir
-	| PrintModules -> str"Print Modules"
-	| PrintMLLoadPath -> str"Print ML Path"
-	| PrintMLModules -> str"Print ML Modules"
-	| PrintGraph -> str"Print Graph"
-	| PrintClasses -> str"Print Classes"
-	| PrintTypeClasses -> str"Print TypeClasses"
-	| PrintInstances qid -> str"Print Instances" ++ spc () ++ pr_smart_global qid
-	| PrintLtac qid -> str"Print Ltac" ++ spc() ++ pr_ltac_ref qid
-	| PrintCoercions -> str"Print Coercions"
-	| PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
-	| PrintCanonicalConversions -> str"Print Canonical Structures"
-	| PrintTables -> str"Print Tables"
-	| PrintHintGoal -> str"Print Hint"
-	| PrintHint qid -> str"Print Hint" ++ spc() ++ pr_smart_global qid
-	| PrintHintDb -> str"Print Hint *"
-	| PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s
-	| PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s
-	| PrintUniverses (b, fopt) -> Printf.ksprintf str "Print %sUniverses" (if b then "Sorted " else "") ++ pr_opt str fopt
-	| PrintName qid -> str"Print" ++ spc()  ++ pr_smart_global qid
-	| PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid
-	| PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid
-	| PrintInspect n -> str"Inspect" ++ spc() ++ int n
-	| PrintScopes -> str"Print Scopes"
-	| PrintScope s -> str"Print Scope" ++ spc() ++ str s
-	| PrintVisibility s -> str"Print Visibility" ++ pr_opt str s
-	| PrintAbout qid -> str"About" ++ spc()  ++ pr_smart_global qid
-	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_smart_global qid
-(* spiwack: command printing all the axioms and section variables used in a
-         term *)
-	| PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
-	    ++ spc() ++ pr_smart_global qid
-	| PrintNamespace dp -> str"Print Namespace" ++ pr_dirpath dp
-      in pr_printable p
+  | VernacPrint p -> pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc ->
       let pr_locate =function
diff --git a/printing/printer.ml b/printing/printer.ml
index 74c5a02d5f..7d9d27e81b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -586,19 +586,24 @@ let pr_assumptionset env s =
       try str " : " ++ pr_ltype typ with _ -> mt ()
     in
     let fold t typ accu =
-      let (v, a, o) = accu in
+      let (v, a, o, tr) = accu in
       match t with
       | Variable id ->
         let var = str (string_of_id id) ++ str " : " ++ pr_ltype typ in
-        (var :: v, a, o)
+        (var :: v, a, o, tr)
       | Axiom kn ->
         let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
-        (v, ax :: a, o)
+        (v, ax :: a, o, tr)
       | Opaque kn ->
         let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
-        (v, a, opq :: o)
+        (v, a, opq :: o, tr)
+      | Transparent kn ->
+        let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in
+        (v, a, o, tran :: tr)
+    in
+    let (vars, axioms, opaque, trans) = 
+      ContextObjectMap.fold fold s ([], [], [], [])
     in
-    let (vars, axioms, opaque) = ContextObjectMap.fold fold s ([], [], []) in
     let opt_list title = function
     | [] -> None
     | l ->
@@ -608,6 +613,7 @@ let pr_assumptionset env s =
       Some section
     in
     let assums = [
+      opt_list (str "Transparent constants:") trans;
       opt_list (str "Section Variables:") vars;
       opt_list (str "Axioms:") axioms;
       opt_list (str "Opaque constants:") opaque;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fa00689982..42c36f5192 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1377,12 +1377,13 @@ let vernac_print = function
     msg_notice (print_about qid)
   | PrintImplicit qid ->
     dump_global qid; msg_notice (print_impargs qid)
-  | PrintAssumptions (o,r) ->
+  | PrintAssumptions (o,t,r) ->
       (* Prints all the axioms and section variables used by a term *)
       let cstr = constr_of_global (smart_global r) in
       let st = Conv_oracle.get_transp_state () in
-      let nassums = Assumptions.assumptions st ~add_opaque:o cstr in
-      msg_notice (Printer.pr_assumptionset (Global.env ()) nassums)
+      let nassums =
+	Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in
+      msg (Printer.pr_assumptionset (Global.env ()) nassums)
 
 let global_module r =
   let (loc,qid) = qualid_of_reference r in