From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 22 Jan 2004 10:24:50 +0000 (+0000)
Subject: - bugfix: print metas local context in the rigth order
X-Git-Tag: V_0_5_1_3~12
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3eca59409abc3dc4a3c4b07752282fb47e2a5c30;p=helm.git

- bugfix: print metas local context in the rigth order
- renamed string_of_name to ppname and exported it
---

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index a8d9eaa0b..5c5bd71ff 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -41,7 +41,7 @@ exception NotEnoughElements;;
 
 (* Utility functions *)
 
-let string_of_name =
+let ppname =
  function
     Cic.Name s     -> s
   | Cic.Anonymous  -> "_"
@@ -79,7 +79,7 @@ let rec pp t l =
     | C.Meta (n,l1) ->
        "?" ^ (string_of_int n) ^ "[" ^ 
         String.concat " ; "
-         (List.map (function None -> "_" | Some t -> pp t l) l1) ^
+         (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
         "]"
     | C.Sort s ->
        (match s with
@@ -96,9 +96,9 @@ let rec pp t l =
        )
     | C.Cast (v,t) -> pp v l
     | C.Lambda (b,s,t) ->
-       "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
     | C.LetIn (b,s,t) ->
-       "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
@@ -226,11 +226,11 @@ let ppobj obj =
 	            (match context_entry with
 	                Some (n,C.Decl at) ->
                    (separate i) ^
-                     string_of_name n ^ ":" ^ pp at name_context ^ " ",
+                     ppname n ^ ":" ^ pp at name_context ^ " ",
                       (Some n)::name_context
 	              | Some (n,C.Def (at,None)) ->
                    (separate i) ^
-                     string_of_name n ^ ":= " ^ pp at name_context ^ " ",
+                     ppname n ^ ":= " ^ pp at name_context ^ " ",
                       (Some n)::name_context
                 | None ->
                    (separate i) ^ "_ :? _ ", None::name_context
diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli
index 9f68d0525..371b75e29 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.mli
+++ b/helm/ocaml/cic_proof_checking/cicPp.mli
@@ -45,3 +45,6 @@ val ppterm : Cic.term -> string
 (* Required only by the topLevel. It is the generalization of ppterm to *)
 (* work with environments.                                              *)
 val pp : Cic.term -> (Cic.name option) list -> string
+
+val ppname : Cic.name -> string
+