X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=5870089beda2d9f208f318cbd22789d87a60c73f;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=dfa47e469bbd97d12ddbf6e83ce39935bd90c526;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index dfa47e469..5870089be 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open Printf
 
 (* PROFILING *)
@@ -191,8 +193,8 @@ let apply_subst_gen ~appl_fun subst term =
             List.map (function None -> None | Some t -> Some (um_aux t)) l
           in
            C.Meta (i,l'))
-    | C.Sort _ as t -> t
-    | C.Implicit _ -> assert false
+    | C.Sort _
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
@@ -228,7 +230,7 @@ let apply_subst_gen ~appl_fun subst term =
        in
        C.CoFix (i, fl')
  in
- um_aux term
+  LibrarySync.merge_coercions (um_aux term)
 ;;
 
 let apply_subst =
@@ -288,9 +290,15 @@ let apply_subst_metasenv subst metasenv =
 
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
-let ppterm_in_context subst term name_context =
+let ppterm_in_name_context subst term name_context =
  CicPp.pp (apply_subst subst term) name_context
 
+let ppterm_in_context subst term context =
+ let name_context =
+  List.map (function None -> None | Some (n,_) -> Some n) context
+ in
+  ppterm_in_name_context subst term name_context
+
 let ppcontext' ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
@@ -298,13 +306,13 @@ let ppcontext' ?(sep = "\n") subst context =
      match context_entry with
         Some (n,Cic.Decl t) ->
          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_context subst t name_context), (Some n)::name_context
+          (ppterm_in_name_context subst t name_context), (Some n)::name_context
       | Some (n,Cic.Def (bo,ty)) ->
          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
           (match ty with
               None -> "_"
-            | Some ty -> ppterm_in_context subst ty name_context)
-          (ppterm_in_context subst bo name_context), (Some n)::name_context
+            | Some ty -> ppterm_in_name_context subst ty name_context)
+          (ppterm_in_name_context subst bo name_context), (Some n)::name_context
        | None ->
           sprintf "%s_ :? _" (separate i), None::name_context
     ) context ("",[])
@@ -315,7 +323,7 @@ let ppsubst_unfolded subst =
       (fun (idx, (c, t,_)) ->
         let context,name_context = ppcontext' ~sep:"; " subst c in
          sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_context subst t name_context))
+          (ppterm_in_name_context subst t name_context))
        subst)
 (* 
         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
@@ -328,7 +336,7 @@ let ppsubst subst =
       (fun (idx, (c, t, _)) ->
         let context,name_context = ppcontext' ~sep:"; " [] c in
          sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_context [] t name_context))
+          (ppterm_in_name_context [] t name_context))
        subst)
 ;;
 
@@ -340,7 +348,7 @@ let ppmetasenv ?(sep = "\n") subst metasenv =
       (fun (i, c, t) ->
         let context,name_context = ppcontext' ~sep:"; " subst c in
          sprintf "%s |- ?%d: %s" context i
-          (ppterm_in_context subst t name_context))
+          (ppterm_in_name_context subst t name_context))
       (List.filter
         (fun (i, _, _) -> not (List.mem_assoc i subst))
         metasenv))