From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 6 May 2010 15:50:07 +0000 (+0000)
Subject: Fixing naming scheme for composite coercions.
X-Git-Tag: make_still_working~2910
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=668fb315dc8502dc1b4d336eba19ab9436bf5b7a;p=helm.git

Fixing naming scheme for composite coercions.
---

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
index fa6b163ad..28aa0adf0 100644
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-let debug s = prerr_endline (Lazy.force s) ;;
+(* let debug s = prerr_endline (Lazy.force s) ;;*)
 let debug _ = ();;
 
 let skel_dummy = NCic.Implicit `Type;;
@@ -127,7 +127,7 @@ let only_head = function
 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
   let status, src, cpos = 
     let rec aux cpos ctx = function
-      | NCic.Prod (name,ty,bo) ->
+      | NCic.Prod (name,ty,bo) -> 
          if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
          else
            (try 
@@ -195,13 +195,13 @@ let close_graph name t s d to_s from_d p a status =
     let c_o_from_d = 
       product 
         (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) -> 
-          compose_names n1 n,m1@mc,t1,[i,c],j,count_prod ty) 
+          compose_names n n1,m1@mc,t1,[i,c],j,count_prod ty) 
         [c] from_d
     in
     let to_s_o_c_o_from_d =
       product 
         (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)-> 
-          compose_names n n1,m@m1,t,(i,t1)::upl,j,a)
+          compose_names n1 n,m@m1,t,(i,t1)::upl,j,a)
         to_s c_o_from_d
     in
     to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
@@ -231,7 +231,7 @@ let close_graph name t s d to_s from_d p a status =
          let src = only_head src in
          let tgt = only_head tgt in
          debug (lazy(
-           "composite: "^
+           "composite " ^ name ^ ": "^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^