From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Sep 2008 12:04:47 +0000 (+0000)
Subject: ppterm_in_named_context removed in favour of the high-level pretty printer.
X-Git-Tag: make_still_working~4771
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=48cf38fbbfcb60e6b64e5157801bc421677e71be;p=helm.git

ppterm_in_named_context removed in favour of the high-level pretty printer.
Much nicer error messages :-)
---

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 6d187432a..8db1cf82f 100644
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -300,14 +300,11 @@ match subst with
 let ppterm ~metasenv subst term =
  CicPp.ppterm ~metasenv (apply_subst subst term)
 
-let ppterm_in_name_context ~metasenv subst term name_context =
- CicPp.pp ~metasenv (apply_subst subst term) name_context
-
 let ppterm_in_context ~metasenv subst term context =
  let name_context =
   List.map (function None -> None | Some (n,_) -> Some n) context
  in
-  ppterm_in_name_context ~metasenv subst term name_context
+  CicPp.pp ~metasenv (apply_subst subst term) name_context
 
 let ppterm_in_context_ref = ref ppterm_in_context
 let set_ppterm_in_context f =
@@ -323,28 +320,29 @@ let ppterm_in_context ~metasenv subst term context =
 let ppcontext' ~metasenv ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
-   (fun context_entry (i,name_context) ->
+   (fun context_entry (i,context) ->
      match context_entry with
         Some (n,Cic.Decl t) ->
          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_name_context ~metasenv subst t name_context),
-          (Some n)::name_context
+          (ppterm_in_context ~metasenv subst t context),
+          context_entry::context
       | Some (n,Cic.Def (bo,ty)) ->
          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_name_context ~metasenv subst ty name_context)
-          (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
+          (ppterm_in_context ~metasenv subst ty context)
+          (ppterm_in_context ~metasenv subst bo context),
+          context_entry::context
        | None ->
-          sprintf "%s_ :? _" (separate i), None::name_context
+          sprintf "%s_ :? _" (separate i), context_entry::context
     ) context ("",[])
 
 let ppsubst_unfolded ~metasenv subst =
   String.concat "\n"
     (List.map
       (fun (idx, (c, t,ty)) ->
-        let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
-         sprintf "%s |- ?%d : %s := %s" context idx
-(ppterm_in_name_context ~metasenv [] ty name_context)
-          (ppterm_in_name_context ~metasenv subst t name_context))
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+         sprintf "%s |- ?%d : %s := %s" scontext idx
+(ppterm_in_context ~metasenv [] ty context)
+          (ppterm_in_context ~metasenv subst t context))
        subst)
 (* 
         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
@@ -355,9 +353,9 @@ let ppsubst ~metasenv subst =
   String.concat "\n"
     (List.map
       (fun (idx, (c, t, ty)) ->
-        let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
-         sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context)
-          (ppterm_in_name_context ~metasenv [] t name_context))
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " [] c in
+         sprintf "%s |- ?%d : %s := %s" scontext idx (ppterm_in_context ~metasenv [] ty context)
+          (ppterm_in_context ~metasenv [] t context))
        subst)
 ;;
 
@@ -368,9 +366,9 @@ let ppmetasenv ?(sep = "\n") subst metasenv =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
-        let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
-         sprintf "%s |- ?%d: %s" context i
-          (ppterm_in_name_context ~metasenv subst t name_context))
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+         sprintf "%s |- ?%d: %s" scontext i
+          (ppterm_in_context ~metasenv subst t context))
       (List.filter
         (fun (i, _, _) -> not (List.mem_assoc i subst))
         metasenv))
diff --git a/helm/software/components/cic_unification/cicMetaSubst.mli b/helm/software/components/cic_unification/cicMetaSubst.mli
index bc5b4c039..0d2a08d55 100644
--- a/helm/software/components/cic_unification/cicMetaSubst.mli
+++ b/helm/software/components/cic_unification/cicMetaSubst.mli
@@ -71,9 +71,6 @@ val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string
 val ppcontext:
  metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context ->
    string
-val ppterm_in_name_context:
- metasenv:Cic.metasenv -> Cic.substitution -> Cic.term ->
-  (Cic.name option) list -> string
 val ppterm_in_context:
  metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string
 val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string