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

1 files changed, 21 insertions, 11 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 232551984b..404e1b6ae7 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 ()
 			     )
 			 )