From 668fb315dc8502dc1b4d336eba19ab9436bf5b7a Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 6 May 2010 15:50:07 +0000 Subject: [PATCH] Fixing naming scheme for composite coercions. --- .../components/grafite_engine/nCicCoercDeclaration.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 ^ " ===> " ^ -- 2.39.2