X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicMetaSubst.ml;h=a361b7a32bc3a9ee6fe1c8a1bc24fd4c6095a81b;hb=65c0b57c0b8566b4cb256ec2533554b9c5105b8c;hp=c097eacf281869b9ff532d8e127ec80ac5d75d82;hpb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;p=helm.git

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index c097eacf2..a361b7a32 100644
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -305,6 +305,17 @@ let ppterm_in_context ~metasenv subst term context =
  in
   ppterm_in_name_context ~metasenv subst term name_context
 
+let ppterm_in_context_ref = ref ppterm_in_context
+let set_ppterm_in_context f =
+ ppterm_in_context_ref := f
+let use_low_level_ppterm_in_context = ref false
+
+let ppterm_in_context ~metasenv subst term context =
+ if !use_low_level_ppterm_in_context then
+  ppterm_in_context ~metasenv subst term context
+ else
+  !ppterm_in_context_ref ~metasenv subst term context
+
 let ppcontext' ~metasenv ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
@@ -327,9 +338,10 @@ let ppcontext' ~metasenv ?(sep = "\n") subst context =
 let ppsubst_unfolded ~metasenv subst =
   String.concat "\n"
     (List.map
-      (fun (idx, (c, t,_)) ->
+      (fun (idx, (c, t,ty)) ->
         let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
-         sprintf "%s |- ?%d:= %s" context idx
+         sprintf "%s |- ?%d : %s := %s" context idx
+(ppterm_in_name_context ~metasenv [] ty name_context)
           (ppterm_in_name_context ~metasenv subst t name_context))
        subst)
 (* 
@@ -340,9 +352,9 @@ let ppsubst_unfolded ~metasenv subst =
 let ppsubst ~metasenv subst =
   String.concat "\n"
     (List.map
-      (fun (idx, (c, t, _)) ->
+      (fun (idx, (c, t, ty)) ->
         let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
-         sprintf "%s |- ?%d:= %s" context idx
+         sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context)
           (ppterm_in_name_context ~metasenv [] t name_context))
        subst)
 ;;
@@ -629,7 +641,7 @@ let delift n subst context metasenv l t =
          if m <=k then
           C.Rel m
          else
-          (try
+           (try
             match List.nth context (m-k-1) with
                Some (_,C.Def (t,_)) ->
                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
@@ -643,7 +655,7 @@ let delift n subst context metasenv l t =
                 C.Rel ((position (m-k) l) + k)
              | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
            with
-            Failure _ ->
+            Failure _ -> 
              raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
           )
      | C.Var (uri,exp_named_subst) ->