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 6d187432ae12ba7e73789d4af25719eedc6e637e..8db1cf82f31c3759a33cb4f5b14e850d2a5c6c22 100644 (file)
--- 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 bc5b4c0390b480dc20ee3379713510e9e4a3124b..0d2a08d55223f19f2e50d1446f271813e83e7682 100644 (file)
--- 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