IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).

MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.

KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.


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

1 files changed, 14 insertions, 5 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 870d382f8..41151eb22 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -59,7 +59,7 @@ let prastpat c = pp(print_astpat c)
 let prastpatl c = pp(print_astlpat c)
 
 let safe_prglobal = function 
-  | ConstRef kn -> pp (str "CONSTREF(" ++ pr_kn kn ++ str ")")
+  | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")")
   | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
 			  int i ++ str ")")
   | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
@@ -119,7 +119,7 @@ let constr_display csr =
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
   | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
-  | Const c -> "Const("^(string_of_kn c)^")"
+  | Const c -> "Const("^(string_of_con c)^")"
   | Ind (sp,i) ->
       "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")"
   | Construct ((sp,i),j) ->
@@ -200,7 +200,7 @@ let print_pure_constr csr =
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string"}"
   | Const c -> print_string "Cons(";
-      sp_display c;
+      sp_con_display c;
       print_string ")"
   | Ind (sp,i) ->
       print_string "Ind(";
@@ -273,6 +273,15 @@ let print_pure_constr csr =
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
       print_string (string_of_kn sp)
+  and sp_con_display sp = 
+(*    let dir,l = decode_kn sp in
+    let ls = 
+      match List.rev (List.map string_of_id (repr_dirpath dir)) with 
+          ("Top"::l)-> l
+	| ("Coq"::_::l) -> l 
+	| l             -> l
+    in  List.iter (fun x -> print_string x; print_string ".") ls;*)
+      print_string (string_of_con sp)
 
   in
     try 
@@ -317,7 +326,7 @@ let ppripos (ri,pos) =
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
-      print_string ("getglob "^(string_of_kn kn)^"\n"));
+      print_string ("getglob "^(string_of_con kn)^"\n"));
    print_flush ()
 
 let print_vfix () = print_string "vfix"
@@ -335,7 +344,7 @@ let print_idkey idk =
   match idk with 
   | ConstKey sp -> 
       print_string "Cons(";
-      print_string (string_of_kn sp);
+      print_string (string_of_con sp);
       print_string ")"
   | VarKey id -> print_string (string_of_id id)
   | RelKey i -> print_string "~";print_int i