X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicMetaSubst.ml;h=8db1cf82f31c3759a33cb4f5b14e850d2a5c6c22;hb=e79fd328fe626dbd8c76183c36f721119e9fb668;hp=6d187432ae12ba7e73789d4af25719eedc6e637e;hpb=d70d83df962621feeb0e674810a1b9583c7e5487;p=helm.git

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))