From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 15 Feb 2006 13:04:35 +0000 (+0000)
Subject: added support for "polymorphic" coercions
X-Git-Tag: make_still_working~7562
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=185bfc8f9c9ba49308477ee6769701f3e2977115;p=helm.git

added support for "polymorphic" coercions
---

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 5870089be..53efcf96e 100644
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -1,4 +1,5 @@
 (* Copyright (C) 2003, HELM Team.
+ * 
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -230,7 +231,7 @@ let apply_subst_gen ~appl_fun subst term =
        in
        C.CoFix (i, fl')
  in
-  LibrarySync.merge_coercions (um_aux term)
+  um_aux term
 ;;
 
 let apply_subst =
diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 620f66f18..b74d40296 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -58,7 +58,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn =
    Cic.CicHash.find localization_tbl t
   with Not_found ->
    prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
-   assert false
+   raise exn'
  in
   raise (HExtlib.Localized (loc,exn'))
 
@@ -81,19 +81,80 @@ let rec split l n =
 let exp_impl metasenv subst context =
  function
   | Some `Type ->
-        let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
-        let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-        metasenv', Cic.Meta (idx, irl)
+      let (metasenv', idx) = 
+        CicMkImplicit.mk_implicit_type metasenv subst context in
+      let irl = 
+        CicMkImplicit.identity_relocation_list_for_metavariable context in
+      metasenv', Cic.Meta (idx, irl)
   | Some `Closed ->
-        let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
-        metasenv', Cic.Meta (idx, [])
+      let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
+      metasenv', Cic.Meta (idx, [])
   | None ->
-        let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
-        let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-        metasenv', Cic.Meta (idx, irl)
+      let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
+      let irl = 
+        CicMkImplicit.identity_relocation_list_for_metavariable context in
+      metasenv', Cic.Meta (idx, irl)
   | _ -> assert false
 ;;
 
+let is_a_double_coercion t =
+  let last_of l = 
+    let rec aux = function
+      | x::[] -> x
+      | x::tl -> aux tl
+      | [] -> assert false
+    in
+    aux l
+  in
+  let dummyres = 
+    false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None 
+  in
+  match t with
+  | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
+      (match last_of tl with
+      | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
+          let head = last_of tl2 in
+          true, c1, c2, head 
+      | _ -> dummyres)
+  | _ -> dummyres
+  
+let avoid_double_coercion context subst metasenv ugraph t ty = 
+  let arity_of con =
+    try
+      let ty,_=CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
+      let rec count_pi = function
+        | Cic.Prod (_,_,t) -> 1 + count_pi t
+        | _ -> 0
+      in
+      count_pi ty
+    with Invalid_argument _ -> assert false (* all coercions have an uri *)
+  in
+  let rec mk_implicits tail = function
+    | 0 -> [tail] 
+    | n -> Cic.Implicit None :: mk_implicits tail (n-1)
+  in
+  let b, c1, c2, head = is_a_double_coercion t in
+  if b then
+    let source_carr = CoercGraph.source_of c2 in
+    let tgt_carr = CicMetaSubst.apply_subst subst ty in
+    (match CoercGraph.look_for_coercion source_carr tgt_carr 
+    with
+    | CoercGraph.SomeCoercion c -> 
+        let arity = arity_of c in
+        let args = mk_implicits head (arity - 1) in
+        let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in
+        let newt = Cic.Appl (c_bo::args) in
+        let subst, metasenv, ugraph = 
+          CicUnification.fo_unif_subst subst context metasenv newt t ugraph
+        in
+        debug_print 
+          (lazy 
+            ("packing: " ^ 
+              CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
+        Cic.Appl (c::args), ty, subst, metasenv, ugraph
+    | _ -> assert false) (* the composite coercion must exist *)
+  else
+    t, ty, subst, metasenv, ugraph  
 
 let rec type_of_constant uri ugraph =
  let module C = Cic in
@@ -110,7 +171,8 @@ let rec type_of_constant uri ugraph =
     | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
     | _ ->
        raise
-        (RefineFailure (lazy ("Unknown constant definition " ^  U.string_of_uri uri)))
+        (RefineFailure 
+          (lazy ("Unknown constant definition " ^  U.string_of_uri uri)))
 
 and type_of_variable uri ugraph =
   let module C = Cic in
@@ -345,7 +407,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                            subst coercion_src context ^ " that is not a sort")))
                     | CoercGraph.SomeCoercion c -> 
                        let newt, tty, subst, metasenv, ugraph = 
-                         avoid_double_coercion 
+                         avoid_double_coercion context
                           subst metasenv ugraph
                             (Cic.Appl[c;t]) coercion_tgt
                        in
@@ -389,7 +451,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       match boh with
                       | CoercGraph.SomeCoercion c -> 
                         let newt, tty, subst', metasenv', ugraph1 = 
-                          avoid_double_coercion 
+                          avoid_double_coercion context
                            subst' metasenv' ugraph1 
                              (Cic.Appl[c;s']) coercion_tgt 
                         in
@@ -452,7 +514,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               eat_prods true subst'' metasenv'' context 
                 hetype tlbody_and_type ugraph2
             in
-              avoid_double_coercion 
+              avoid_double_coercion context 
                 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
         | C.Appl _ -> assert false
         | C.Const (uri,exp_named_subst) ->
@@ -851,19 +913,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       relocalize localization_tbl t t';
       res
 
-  and  avoid_double_coercion subst metasenv ugraph t ty = 
-    match t with
-    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when 
-      CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
-          let source_carr = CoercGraph.source_of c2 in
-          let tgt_carr = CicMetaSubst.apply_subst subst ty in
-          (match CoercGraph.look_for_coercion source_carr tgt_carr 
-          with
-          | CoercGraph.SomeCoercion c -> 
-              Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph
-          | _ -> assert false) (* the composite coercion must exist *)
-    | _ -> t, ty, subst, metasenv, ugraph
-
   (* check_metasenv_consistency checks that the "canonical" context of a
      metavariable is consitent - up to relocation via the relocation list l -
      with the actual context *)
@@ -1059,7 +1108,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       try
         fo_unif_subst subst context metasenv hetype hetype' ugraph
       with exn ->
-        debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+        debug_print 
+          (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
                          (CicPp.ppterm hetype)
                          (CicPp.ppterm hetype')
                          (CicMetaSubst.ppmetasenv [] metasenv)
@@ -1113,7 +1163,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                                  (* "\nReason: " ^ Lazy.force e*))))
                        | CoercGraph.SomeCoercion c -> 
                            let newt, _, subst, metasenv, ugraph = 
-                             avoid_double_coercion 
+                             avoid_double_coercion context
                               subst metasenv ugraph 
                                 (Cic.Appl[c;hete]) tgt_carr in
                            try
@@ -1365,6 +1415,158 @@ let typecheck metasenv uri obj ~localization_tbl =
        are_all_occurrences_positive metasenv ugraph uri tys paramsno 
      in
      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
+;;
+
+(* sara' piu' veloce che raffinare da zero? mah.... *)
+let pack_coercion metasenv t =
+ let module C = Cic in
+ let rec merge_coercions ctx =
+   let aux = (fun (u,t) -> u,merge_coercions ctx t) in
+   function
+   | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
+   | C.Meta (n,subst) ->
+      let subst' =
+       List.map
+        (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
+      in
+       C.Meta (n,subst')
+   | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
+   | C.Prod (name,so,dest) -> 
+       let ctx' = (Some (name,C.Decl so))::ctx in
+       C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest) 
+   | C.Lambda (name,so,dest) -> 
+       let ctx' = (Some (name,C.Decl so))::ctx in
+       C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
+   | C.LetIn (name,so,dest) -> 
+       let ctx' = Some (name,(C.Def (so,None)))::ctx in
+       C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
+   | C.Appl l as t -> 
+       let b,_,_,_ = is_a_double_coercion t in
+       (* prerr_endline "CANDIDATO!!!!"; *)
+       let newt = 
+         if b then
+           let ugraph = CicUniv.empty_ugraph in
+           let old_insert_coercions = !insert_coercions in
+           insert_coercions := false;
+           let newt, _, menv, _ = 
+             try 
+               type_of_aux' metasenv ctx t ugraph 
+             with RefineFailure _ | Uncertain _ -> 
+               prerr_endline (CicPp.ppterm t);
+               t, t, [], ugraph 
+           in
+           insert_coercions := old_insert_coercions;
+           if metasenv <> [] || menv = [] then 
+             newt 
+           else 
+             (prerr_endline "PUO' SUCCEDERE!!!!!";t)
+         else
+           t
+       in
+       (match newt with
+       | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
+       | _ -> assert false)
+   | C.Var (uri,exp_named_subst) -> 
+       let exp_named_subst = List.map aux exp_named_subst in
+       C.Var (uri, exp_named_subst)
+   | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst = List.map aux exp_named_subst in
+       C.Const (uri, exp_named_subst)
+   | C.MutInd (uri,tyno,exp_named_subst) ->
+       let exp_named_subst = List.map aux exp_named_subst in
+       C.MutInd (uri,tyno,exp_named_subst)
+   | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+       let exp_named_subst = List.map aux exp_named_subst in
+       C.MutConstruct (uri,tyno,consno,exp_named_subst)  
+   | C.MutCase (uri,tyno,out,te,pl) ->
+       let pl = List.map (merge_coercions ctx) pl in
+       C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
+   | C.Fix (fno, fl) ->
+       let ctx =
+         List.fold_left
+           (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) 
+           ctx fl
+       in 
+       let fl = 
+         List.map 
+           (fun (name,idx,ty,bo) -> 
+             (name,idx,merge_coercions ctx ty,merge_coercions ctx bo)) 
+         fl
+       in
+       C.Fix (fno, fl)
+   | C.CoFix (fno, fl) ->
+       let ctx =
+         List.fold_left
+           (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) 
+           ctx fl
+       in 
+       let fl = 
+         List.map 
+           (fun (name,ty,bo) -> 
+             (name, merge_coercions ctx ty, merge_coercions ctx bo)) 
+         fl 
+       in
+       C.CoFix (fno, fl)
+ in
+ merge_coercions [] t
+;;
+
+let pack_coercion_obj obj =
+  let module C = Cic in
+  match obj with
+  | C.Constant (id, body, ty, params, attrs) -> 
+      let body = 
+        match body with 
+        | None -> None 
+        | Some body -> Some (pack_coercion [] body) 
+      in
+      let ty = pack_coercion [] ty in
+        C.Constant (id, body, ty, params, attrs)
+  | C.Variable (name, body, ty, params, attrs) ->
+      let body = 
+        match body with 
+        | None -> None 
+        | Some body -> Some (pack_coercion [] body) 
+      in
+      let ty = pack_coercion [] ty in
+        C.Variable (name, body, ty, params, attrs)
+  | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
+      let conjectures = 
+        List.map 
+          (fun (i, ctx, ty) -> 
+            let ctx = 
+              List.map 
+                (function 
+                | Some (name, C.Decl t) -> 
+                    Some (name, C.Decl (pack_coercion conjectures t))
+                | Some (name, C.Def (t,None)) -> 
+                    Some (name, C.Def (pack_coercion conjectures t, None))
+                | Some (name, C.Def (t,Some ty)) -> 
+                    Some (name, C.Def (pack_coercion conjectures t, 
+                                    Some (pack_coercion conjectures ty)))
+                | None -> None) 
+                ctx 
+            in
+            ((i,ctx,pack_coercion conjectures ty))) 
+          conjectures
+      in
+      let body = pack_coercion conjectures body in
+      let ty = pack_coercion conjectures ty in
+      C.CurrentProof (name, conjectures, body, ty, params, attrs)
+  | C.InductiveDefinition (indtys, params, leftno, attrs) ->
+      let indtys = 
+        List.map 
+          (fun (name, ind, arity, cl) -> 
+            let arity = pack_coercion [] arity in
+            let cl = 
+              List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl 
+            in
+            (name, ind, arity, cl))
+          indtys
+      in
+        C.InductiveDefinition (indtys, params, leftno, attrs)
+;;
+
 
 (* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =
diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli
index 224a7586c..c3ab49e0a 100644
--- a/helm/software/components/cic_unification/cicRefine.mli
+++ b/helm/software/components/cic_unification/cicRefine.mli
@@ -46,3 +46,6 @@ val typecheck :
 
 val insert_coercions: bool ref (* initially true *)
 
+(* given a closed term returns it with all coercions packed *)
+val pack_coercion_obj: Cic.obj -> Cic.obj
+
diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index c55bf8d9e..26fc540d8 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -392,11 +392,34 @@ type 'a eval_from_moo =
 let coercion_moo_statement_of uri =
   GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
 
+let refinement_toolkit = {
+  RefinementTool.type_of_aux' = 
+    (fun ?localization_tbl e c t u ->
+      let saved = !CicRefine.insert_coercions in 
+      CicRefine.insert_coercions:= false;
+      let rc = 
+        try 
+          let t, ty, metasenv, ugraph = 
+            CicRefine.type_of_aux' ?localization_tbl e c t u in
+          RefinementTool.Success (t, ty, metasenv, ugraph)
+        with
+        | CicRefine.RefineFailure s
+        | CicRefine.Uncertain s 
+        | CicRefine.AssertFailure s -> RefinementTool.Exception s
+      in
+      CicRefine.insert_coercions := saved;
+      rc);
+  RefinementTool.ppsubst = CicMetaSubst.ppsubst;
+  RefinementTool.apply_subst = CicMetaSubst.apply_subst; 
+  RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; 
+  RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
+ }
+  
 let eval_coercion status ~add_composites uri =
  let basedir = Helm_registry.get "matita.basedir" in
  let status,compounds =
    prerr_endline "evaluating a coercion command";
-  GrafiteSync.add_coercion ~basedir ~add_composites status uri in
+  GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in
  let moo_content = coercion_moo_statement_of uri in
  let status = GrafiteTypes.add_moo_content [moo_content] status in
   {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
@@ -505,10 +528,11 @@ let add_coercions_of_record_to_moo obj lemmas status =
             | _ -> None) 
           fields
       in
+      (*
       prerr_endline "wanted coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        wanted_coercions;
+        wanted_coercions; *)
       let coercions, moo_content = 
         List.split
           (HExtlib.filter_map 
@@ -521,10 +545,10 @@ let add_coercions_of_record_to_moo obj lemmas status =
                 None) 
             lemmas)
       in
-      prerr_endline "actual coercions:";
+      (* prerr_endline "actual coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        coercions;
+        coercions; *)
       let status = GrafiteTypes.add_moo_content moo_content status in 
       {status with 
         GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, 
@@ -532,7 +556,7 @@ let add_coercions_of_record_to_moo obj lemmas status =
 
 let add_obj uri obj status =
  let basedir = Helm_registry.get "matita.basedir" in
- let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in
+ let status,lemmas = GrafiteSync.add_obj ~basedir refinement_toolkit uri obj status in
  status, lemmas 
       
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index 37a3132e7..f23b42ecc 100644
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -27,13 +27,13 @@
 
 open Printf
 
-let add_obj ~basedir uri obj status =
- let lemmas = LibrarySync.add_obj uri obj basedir in
+let add_obj refinement_toolkit ~basedir uri obj status =
+ let lemmas = LibrarySync.add_obj refinement_toolkit uri obj basedir in
   {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects},
    lemmas
 
-let add_coercion ~basedir ~add_composites status uri =
- let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
+let add_coercion refinement_toolkit ~basedir ~add_composites status uri =
+ let compounds = LibrarySync.add_coercion ~add_composites ~basedir refinement_toolkit uri in
   {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
    compounds
  
diff --git a/helm/software/components/grafite_engine/grafiteSync.mli b/helm/software/components/grafite_engine/grafiteSync.mli
index ce3c04250..f686eb2d8 100644
--- a/helm/software/components/grafite_engine/grafiteSync.mli
+++ b/helm/software/components/grafite_engine/grafiteSync.mli
@@ -24,12 +24,15 @@
  *)
 
 val add_obj:
+  RefinementTool.kit ->
   basedir:string -> UriManager.uri -> Cic.obj -> GrafiteTypes.status ->
    GrafiteTypes.status * UriManager.uri list
 
 val add_coercion:
- basedir:string -> add_composites:bool -> GrafiteTypes.status ->
-  UriManager.uri -> GrafiteTypes.status * UriManager.uri list
+  RefinementTool.kit ->
+  basedir:string -> add_composites:bool -> GrafiteTypes.status ->
+  UriManager.uri -> 
+    GrafiteTypes.status * UriManager.uri list
 
 val time_travel: 
   present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
diff --git a/helm/software/components/library/.depend b/helm/software/components/library/.depend
index 5054959da..416a3ce3e 100644
--- a/helm/software/components/library/.depend
+++ b/helm/software/components/library/.depend
@@ -1,4 +1,5 @@
-cicCoercion.cmi: coercDb.cmi 
+cicCoercion.cmi: refinementTool.cmo coercDb.cmi 
+librarySync.cmi: refinementTool.cmo 
 cicElim.cmo: cicElim.cmi 
 cicElim.cmx: cicElim.cmi 
 cicRecord.cmo: cicRecord.cmi 
@@ -9,8 +10,8 @@ libraryDb.cmo: libraryDb.cmi
 libraryDb.cmx: libraryDb.cmi 
 coercDb.cmo: coercDb.cmi 
 coercDb.cmx: coercDb.cmi 
-cicCoercion.cmo: coercDb.cmi cicCoercion.cmi 
-cicCoercion.cmx: coercDb.cmx cicCoercion.cmi 
+cicCoercion.cmo: refinementTool.cmo coercDb.cmi cicCoercion.cmi 
+cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi 
 coercGraph.cmo: coercDb.cmi coercGraph.cmi 
 coercGraph.cmx: coercDb.cmx coercGraph.cmi 
 librarySync.cmo: libraryDb.cmi coercGraph.cmi coercDb.cmi cicRecord.cmi \
diff --git a/helm/software/components/library/Makefile b/helm/software/components/library/Makefile
index 4f0ca3eb8..69a10919d 100644
--- a/helm/software/components/library/Makefile
+++ b/helm/software/components/library/Makefile
@@ -14,6 +14,7 @@ INTERFACE_FILES = \
 	libraryClean.mli \
 	$(NULL)
 IMPLEMENTATION_FILES = \
+	refinementTool.ml \
 	$(INTERFACE_FILES:%.mli=%.ml)
 
 include ../../Makefile.defs
diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index fe636ee35..40def8238 100644
--- a/helm/software/components/library/cicCoercion.ml
+++ b/helm/software/components/library/cicCoercion.ml
@@ -60,35 +60,104 @@ let get_closure_coercions src tgt uri coercions =
 
 let obj_attrs = [`Class `Coercion; `Generated]
 
+exception UnableToCompose
+
 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
-let generate_composite_closure c1 c2 univ =
+let generate_composite_closure rt c1 c2 univ =
+  let module RT = RefinementTool in
   let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
-  let rec mk_rels n =
+  let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in
+  let rec mk_implicits n =
     match n with 
     | 0 -> []
-    | _ -> (Cic.Rel n) :: (mk_rels (n-1))
+    | _ -> (Cic.Implicit None) :: mk_implicits (n-1)
   in
-  let rec compose k =
-    function 
-    | Cic.Prod (name,src,tgt) -> 
-        let name =
-          match name with
-          | Cic.Anonymous -> Cic.Name "x"
-          | _ -> name
-        in
-          Cic.Lambda (name,src,compose (k+1) tgt)
-    | Cic.Appl (he::tl) -> 
-        Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
-    | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
+  let rec mk_lambda_spline c = function
+    | 0 -> c
+    | n -> 
+        Cic.Lambda 
+          (Cic.Name ("A" ^ string_of_int (n-1)), 
+           (Cic.Implicit None), 
+           mk_lambda_spline c (n-1))
+  in 
+  let rec count_saturations_needed n = function
+    | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t
+    | _ -> n
+  in
+  let compose c1 nc1 c2 nc2 =
+    Cic.Lambda 
+      (Cic.Name "x",
+      (Cic.Implicit None),
+      Cic.Appl ( c2 :: mk_implicits nc2 @ 
+        [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ]))
+  in
+  let order_metasenv metasenv = 
+    List.sort 
+      (fun (_,ctx1,_) (_,ctx2,_) -> List.length ctx1 - List.length ctx2) 
+      metasenv
+  in 
+  let rec create_subst_from_metas_to_rels n = function 
+    | [] -> []
+    | (metano, ctx, ty)::tl -> 
+        (metano,(ctx,Cic.Rel (n+1),ty)) ::
+          create_subst_from_metas_to_rels (n-1) tl
+  in
+  let split_metasenv metasenv n =
+    List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv
+  in
+  let purge_unused_lambdas metasenv t =
+    let rec aux = function
+        | Cic.Lambda (_, Cic.Meta (i,_), t) when  
+          List.exists (fun (j,_,_) -> j = i) metasenv ->
+            CicSubstitution.subst (Cic.Rel ~-100) t
+        | Cic.Lambda (name, s, t) -> 
+            Cic.Lambda (name, s, aux t)
+        | t -> t
+    in
+    aux t
   in
-  let c = compose 0 c1_ty in
+  debug_print (lazy ("\nCOMPOSING"));
+  debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
+  debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
+  let saturations_for_c1 = count_saturations_needed 0 c1_ty in 
+  let saturations_for_c2 = count_saturations_needed 0 c2_ty in
+  let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
+  let spline_len = saturations_for_c1 + saturations_for_c2 in
+  let c = mk_lambda_spline c spline_len in
+  (* debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); *)
+  let c, univ = 
+    match rt.RT.type_of_aux' [] [] c univ with
+    | RT.Success (term, ty, metasenv, ugraph) -> 
+        debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
+        let metasenv = order_metasenv metasenv in
+        debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv));
+        let body_metasenv, lambdas_metasenv = 
+          split_metasenv metasenv spline_len 
+        in
+        debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
+        debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv));
+        let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
+        debug_print (lazy("SUBST: "^rt.RT.ppsubst subst));
+        let term = rt.RT.apply_subst subst term in
+        debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
+        (match rt.RT.type_of_aux' metasenv [] term ugraph with
+        | RT.Success (term, ty, metasenv, ugraph) -> 
+            let body_metasenv, lambdas_metasenv = 
+              split_metasenv metasenv spline_len 
+            in
+            let term = purge_unused_lambdas lambdas_metasenv term in
+            debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
+            term, ugraph
+        | RT.Exception s -> debug_print s; raise UnableToCompose)
+    | RT.Exception s -> debug_print s; raise UnableToCompose
+  in  
   let c_ty,univ = 
     try 
       CicTypeChecker.type_of_aux' [] [] c univ
-    with CicTypeChecker.TypeCheckerFailure s as exn ->
+    with CicTypeChecker.TypeCheckerFailure s ->
       debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" 
         (CicPp.ppterm c) (Lazy.force s)));
-      raise exn
+      raise UnableToCompose
   in
   let cleaned_ty =
     FreshNamesGenerator.clean_dummy_dependent_types c_ty 
@@ -110,45 +179,47 @@ let filter_duplicates l coercions =
 (* given a new coercion uri from src to tgt returns 
  * a list of (new coercion uri, coercion obj, universe graph) 
  *)
-let close_coercion_graph src tgt uri =
+let close_coercion_graph rt src tgt uri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
   let todo_list = get_closure_coercions src tgt uri coercions in
   let todo_list = filter_duplicates todo_list coercions in
   let new_coercions = 
-    List.map (
+    HExtlib.filter_map (
       fun (src, l , tgt) ->
-        match l with
-        | [] -> assert false 
-        | he :: tl ->
-            let first_step = 
-              Cic.Constant ("", 
-                Some (CoercDb.term_of_carr (CoercDb.Uri he)),
-                Cic.Sort Cic.Prop, [], obj_attrs)
-            in
-            let o,_ = 
-              List.fold_left (fun (o,univ) coer ->
-                match o with 
-                | Cic.Constant (_,Some c,_,[],_) ->
-                    generate_composite_closure c (CoercDb.term_of_carr (CoercDb.Uri
-                    coer)) univ
+        try 
+          (match l with
+          | [] -> assert false 
+          | he :: tl ->
+              let first_step = 
+                Cic.Constant ("", 
+                  Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+                  Cic.Sort Cic.Prop, [], obj_attrs)
+              in
+              let o,_ = 
+                List.fold_left (fun (o,univ) coer ->
+                  match o with 
+                  | Cic.Constant (_,Some c,_,[],_) ->
+                        generate_composite_closure rt c 
+                          (CoercDb.term_of_carr (CoercDb.Uri coer)) univ
+                  | _ -> assert false 
+                ) (first_step, CicUniv.empty_ugraph) tl
+              in
+              let name_src = CoercDb.name_of_carr src in
+              let name_tgt = CoercDb.name_of_carr tgt in
+              let name = name_tgt ^ "_of_" ^ name_src in
+              let buri = UriManager.buri_of_uri uri in
+              let c_uri = 
+                UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") 
+              in
+              let named_obj = 
+                match o with
+                | Cic.Constant (_,bo,ty,vl,attrs) ->
+                    Cic.Constant (name,bo,ty,vl,attrs)
                 | _ -> assert false 
-              ) (first_step, CicUniv.empty_ugraph) tl
-            in
-            let name_src = CoercDb.name_of_carr src in
-            let name_tgt = CoercDb.name_of_carr tgt in
-            let name = name_tgt ^ "_of_" ^ name_src in
-            let buri = UriManager.buri_of_uri uri in
-            let c_uri = 
-              UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") 
-            in
-            let named_obj = 
-              match o with
-              | Cic.Constant (_,bo,ty,vl,attrs) ->
-                  Cic.Constant (name,bo,ty,vl,attrs)
-              | _ -> assert false 
-            in
-              ((src,tgt,c_uri,named_obj))
+              in
+                Some ((src,tgt,c_uri,named_obj)))
+        with UnableToCompose -> None
     ) todo_list
   in
   new_coercions
diff --git a/helm/software/components/library/cicCoercion.mli b/helm/software/components/library/cicCoercion.mli
index c9eaf0aac..7e4f03ab8 100644
--- a/helm/software/components/library/cicCoercion.mli
+++ b/helm/software/components/library/cicCoercion.mli
@@ -26,6 +26,7 @@
 (* This module implements the Coercions transitive closure *)
 
 val close_coercion_graph:
+  RefinementTool.kit -> 
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
 
diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 8e2c62f31..7203f3647 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -43,14 +43,17 @@ let coerc_carr_of_term t =
     | t -> Term t
 ;;
 
-let name_of_carr = function
+let rec name_of_carr = function
   | Uri u -> UriManager.name_of_uri u
   | Sort s -> CicPp.ppsort s
   | Term (Cic.Appl ((Cic.Const (uri, _))::_)) 
   | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_)) 
   | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) -> 
         UriManager.name_of_uri uri
-  | Term t -> (* CicPp.ppterm t *) assert false
+  | Term (Cic.Prod (_,_,t)) -> name_of_carr (Term t)
+  | Term t -> 
+      prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t); 
+      "FixTheNameMangler"
 
 let eq_carr src tgt =
   match src, tgt with
diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli
index 9e8bf5e9c..1f5df8933 100644
--- a/helm/software/components/library/coercDb.mli
+++ b/helm/software/components/library/coercDb.mli
@@ -32,7 +32,11 @@
 
 
   (** XXX WARNING: non-reentrant *)
-type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+type coerc_carr = 
+  | Uri of UriManager.uri (* const, mutind, mutconstr *)
+  | Sort of Cic.sort (* Prop, Set, Type *) 
+  | Term of Cic.term (* nothing supported *)
+  
 exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
 val eq_carr: coerc_carr -> coerc_carr -> bool
@@ -56,3 +60,4 @@ val is_a_coercion: UriManager.uri -> bool
 val get_carr: UriManager.uri -> coerc_carr * coerc_carr
 
 val term_of_carr: coerc_carr -> Cic.term
+
diff --git a/helm/software/components/library/coercGraph.ml b/helm/software/components/library/coercGraph.ml
index cd958a8f6..62a89b0a7 100644
--- a/helm/software/components/library/coercGraph.ml
+++ b/helm/software/components/library/coercGraph.ml
@@ -94,4 +94,21 @@ let target_of t =
     CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
   with Invalid_argument _ -> assert false (* t must be a coercion *)
     
+let generate_dot_file () =
+  let l = CoercDb.to_list () in
+  let preamble = "
+    digraph pippo {
+      node [fontsize=9, width=.4, height=.4];
+      edge [fontsize=10]; 
+      \n" 
+  in
+  let conclusion = " } \n" in
+  let data = List.fold_left 
+    (fun acc (src,tgt,c) -> 
+      acc ^ CoercDb.name_of_carr src ^ " -> " ^ 
+      CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ 
+      "\"];\n") "" l 
+  in
+  preamble ^ data ^ conclusion
+  
 (* EOF *)
diff --git a/helm/software/components/library/coercGraph.mli b/helm/software/components/library/coercGraph.mli
index 1923a964a..283d8a484 100644
--- a/helm/software/components/library/coercGraph.mli
+++ b/helm/software/components/library/coercGraph.mli
@@ -38,3 +38,4 @@ val is_a_coercion: Cic.term -> bool
 val source_of: Cic.term -> Cic.term
 val target_of: Cic.term -> Cic.term
 
+val generate_dot_file: unit -> string
diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 7363697d5..7209af691 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -37,87 +37,6 @@ let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
  * *)
 let coercion_hashtbl = UriManager.UriHashtbl.create 3
 
-let rec merge_coercions =
- let module C = Cic in
- let aux = (fun (u,t) -> u,merge_coercions t) in
-  function
-     C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
-   | C.Meta (n,subst) ->
-      let subst' =
-       List.map
-        (function None -> None | Some t -> Some (merge_coercions t)) subst
-      in
-       C.Meta (n,subst')
-   | C.Cast (te,ty) -> C.Cast (merge_coercions te, merge_coercions ty)
-   | C.Prod (name,so,dest) -> 
-       C.Prod (name, merge_coercions so, merge_coercions dest) 
-   | C.Lambda (name,so,dest) -> 
-       C.Lambda (name, merge_coercions so, merge_coercions dest)
-   | C.LetIn (name,so,dest) -> 
-       C.LetIn (name, merge_coercions so, merge_coercions dest)
-   | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when 
-     CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
-       let source_carr = CoercGraph.source_of c2 in
-       let tgt_carr = CoercGraph.target_of c1 in
-       (match CoercGraph.look_for_coercion source_carr tgt_carr 
-       with
-       | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
-       | _ -> assert false) (* the composite coercion must exist *)
-   | C.Appl l -> C.Appl (List.map merge_coercions l)
-   | C.Var (uri,exp_named_subst) -> 
-       let exp_named_subst = List.map aux exp_named_subst in
-       C.Var (uri, exp_named_subst)
-   | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst = List.map aux exp_named_subst in
-       C.Const (uri, exp_named_subst)
-   | C.MutInd (uri,tyno,exp_named_subst) ->
-       let exp_named_subst = List.map aux exp_named_subst in
-       C.MutInd (uri,tyno,exp_named_subst)
-   | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-       let exp_named_subst = List.map aux exp_named_subst in
-       C.MutConstruct (uri,tyno,consno,exp_named_subst)  
-   | C.MutCase (uri,tyno,out,te,pl) ->
-       let pl = List.map merge_coercions pl in
-       C.MutCase (uri,tyno,merge_coercions out,merge_coercions te,pl)
-   | C.Fix (fno, fl) ->
-       let fl = List.map (fun (name,idx,ty,bo)->(name,idx,merge_coercions ty,merge_coercions bo)) fl in
-       C.Fix (fno, fl)
-   | C.CoFix (fno, fl) ->
-       let fl = List.map (fun (name,ty,bo) -> (name, merge_coercions ty, merge_coercions bo)) fl in
-       C.CoFix (fno, fl)
-
-let merge_coercions_in_obj obj =
-  let module C = Cic in
-  match obj with
-  | C.Constant (id, body, ty, params, attrs) -> 
-      let body = 
-        match body with 
-        | None -> None 
-        | Some body -> Some (merge_coercions body) 
-      in
-      let ty = merge_coercions ty in
-        C.Constant (id, body, ty, params, attrs)
-  | C.Variable (name, body, ty, params, attrs) ->
-      let body = 
-        match body with 
-        | None -> None 
-        | Some body -> Some (merge_coercions body) 
-      in
-      let ty = merge_coercions ty in
-        C.Variable (name, body, ty, params, attrs)
-  | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) ->
-      assert false
-  | C.InductiveDefinition (indtys, params, leftno, attrs) ->
-      let indtys = 
-        List.map 
-          (fun (name, ind, arity, cl) -> 
-            let arity = merge_coercions arity in
-            let cl = List.map (fun (name, ty) -> (name,merge_coercions ty)) cl in
-            (name, ind, arity, cl))
-          indtys
-      in
-        C.InductiveDefinition (indtys, params, leftno, attrs)
-
 let uris_of_obj uri =
  let innertypesuri = UriManager.innertypesuri_of_uri uri in
  let bodyuri = UriManager.bodyuri_of_uri uri in
@@ -185,12 +104,13 @@ let index_obj =
   fun ~dbd ~uri ->
    profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 
-let add_single_obj uri obj ~basedir =
+let add_single_obj uri obj refinement_toolkit ~basedir =
+  let module RT = RefinementTool in
   let obj = 
     if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
        not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
     then
-      merge_coercions_in_obj obj 
+      refinement_toolkit.RT.pack_coercion_obj obj
     else
       obj 
   in
@@ -253,12 +173,12 @@ let remove_single_obj uri =
 
 (*** GENERATION OF AUXILIARY LEMMAS ***)
 
-let generate_elimination_principles ~basedir uri =
+let generate_elimination_principles ~basedir uri refinement_toolkit =
   let uris = ref [] in
   let elim sort =
     try
       let uri,obj = CicElim.elim_of ~sort uri 0 in
-       add_single_obj uri obj ~basedir;
+       add_single_obj uri obj refinement_toolkit ~basedir;
        uris := uri :: !uris
     with CicElim.Can_t_eliminate -> ()
   in
@@ -275,7 +195,7 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,u1) -> true)
 
-let add_coercion ~basedir ~add_composites uri =
+let add_coercion ~basedir ~add_composites refinement_toolkit uri =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -293,30 +213,30 @@ let add_coercion ~basedir ~add_composites uri =
    *)
   let extract_last_two_p ty =
     let rec aux = function
-      | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> 
-          assert false
-          (* not implemented: aux (Cic.Prod(n,t1,t2)) *)
+      | Cic.Prod( _, _, ((Cic.Prod _) as t)) -> 
+          aux t
       | Cic.Prod( _, src, tgt) -> src, tgt
       | _ -> assert false
     in
     aux ty
   in
   let ty_src, ty_tgt = extract_last_two_p coer_ty in
-  let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
-  let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
-  let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in
+  let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
+  let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
+  let new_coercions = 
+    CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri in
   let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
   (* update the DB *)
   List.iter 
     (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
       new_coercions;
-  CoercDb.add_coercion (src_uri, tgt_uri, uri);
+  CoercDb.add_coercion (src_carr, tgt_carr, uri);
   (* add the composites obj and they eventual lemmas *)
   let lemmas = 
     if add_composites then
       List.fold_left
         (fun acc (_,_,uri,obj) -> 
-          add_single_obj ~basedir uri obj;
+          add_single_obj ~basedir uri obj refinement_toolkit;
           uri::acc) 
         composite_uris new_coercions
     else
@@ -324,9 +244,12 @@ let add_coercion ~basedir ~add_composites uri =
   in
   (* store that composite_uris are related to uri. the first component is the
    * stuff in the DB while the second is stuff for remove_obj *)
-  prerr_endline ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri);
-  List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-      composite_uris;
+  (* 
+     prerr_endline ("adding: " ^ 
+       string_of_bool add_composites ^ UriManager.string_of_uri uri);
+     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+      composite_uris; 
+  *)
   UriManager.UriHashtbl.add coercion_hashtbl uri 
     (composite_uris,if add_composites then composite_uris else []);
   lemmas
@@ -351,7 +274,7 @@ let remove_coercion uri =
     Not_found -> () (* mhh..... *)
     
 
-let generate_projections ~basedir uri fields =
+let generate_projections ~basedir refinement_toolkit uri fields =
  let uris = ref [] in
  let projections = CicRecord.projections_of uri (List.map fst fields) in
   try
@@ -362,10 +285,10 @@ let generate_projections ~basedir uri fields =
          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
        let attrs = [`Class `Projection; `Generated] in
        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
-        add_single_obj ~basedir uri obj;
+        add_single_obj ~basedir uri obj refinement_toolkit;
         let composites = 
          if coercion then
-            add_coercion ~basedir ~add_composites:true uri
+            add_coercion ~basedir ~add_composites:true refinement_toolkit uri
           else  
             []
         in
@@ -386,15 +309,16 @@ let generate_projections ~basedir uri fields =
    raise exn
 
 
-let add_obj uri obj ~basedir =
- add_single_obj uri obj ~basedir;
+let add_obj refinement_toolkit uri obj ~basedir =
+ add_single_obj uri obj refinement_toolkit ~basedir;
  let uris = ref [] in
  try
   begin
    match obj with
     | Cic.Constant _ -> ()
     | Cic.InductiveDefinition (_,_,_,attrs) ->
-        uris := !uris @ generate_elimination_principles ~basedir uri;
+        uris := !uris @ 
+          generate_elimination_principles ~basedir uri refinement_toolkit;
         let rec get_record_attrs =
           function
           | [] -> None
@@ -404,7 +328,8 @@ let add_obj uri obj ~basedir =
          (match get_record_attrs attrs with
          | None -> () (* not a record *)
          | Some fields ->
-            uris := !uris @ (generate_projections ~basedir uri fields))
+            uris := !uris @ 
+              (generate_projections ~basedir refinement_toolkit uri fields))
     | Cic.CurrentProof _
     | Cic.Variable _ -> assert false
   end;
diff --git a/helm/software/components/library/librarySync.mli b/helm/software/components/library/librarySync.mli
index d063b3282..812685c53 100644
--- a/helm/software/components/library/librarySync.mli
+++ b/helm/software/components/library/librarySync.mli
@@ -25,12 +25,13 @@
 
 exception AlreadyDefined of UriManager.uri
 
-val merge_coercions: Cic.term -> Cic.term
-
 (* adds an object to the library together with all auxiliary lemmas on it *)
 (* (e.g. elimination principles, projections, etc.)                       *)
 (* it returns the list of the uris of the auxiliary lemmas generated      *)
-val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> UriManager.uri list
+val add_obj: 
+  RefinementTool.kit -> 
+  UriManager.uri -> Cic.obj -> basedir:string -> 
+    UriManager.uri list
 
 (* inverse of add_obj;                                                   *)
 (* Warning: it does not remove the dependencies on the object and on its *)
@@ -42,7 +43,8 @@ val remove_obj: UriManager.uri -> unit
 (* is true are added to the library.                                     *)
 (* The list of added objects is returned.                                *)
 val add_coercion: 
-  basedir:string -> add_composites:bool -> UriManager.uri -> 
+  basedir:string -> add_composites:bool -> 
+  RefinementTool.kit -> UriManager.uri -> 
     UriManager.uri list
 
 (* inverse of add_coercion, removes both the eventually created composite   *)
diff --git a/helm/software/components/library/refinementTool.ml b/helm/software/components/library/refinementTool.ml
new file mode 100644
index 000000000..70af8740b
--- /dev/null
+++ b/helm/software/components/library/refinementTool.ml
@@ -0,0 +1,41 @@
+(* Copyright (C) 2006, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+type type_of_rc = 
+  | Success of Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph
+  | Exception of string Lazy.t
+
+  (* these are the same functions of cic_unification/ (eventually wrapped) *)
+type kit = {
+  type_of_aux':
+    ?localization_tbl:Token.flocation Cic.CicHash.t ->
+    Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
+      type_of_rc;
+  pack_coercion_obj: Cic.obj -> Cic.obj;
+  apply_subst: Cic.substitution -> Cic.term -> Cic.term ;
+  ppsubst: Cic.substitution -> string;
+  ppmetasenv: Cic.substitution -> Cic.metasenv -> string;
+} 
+
diff --git a/helm/software/components/tactics/proofEngineTypes.ml b/helm/software/components/tactics/proofEngineTypes.ml
index 68ea561f9..4eb043ca8 100644
--- a/helm/software/components/tactics/proofEngineTypes.ml
+++ b/helm/software/components/tactics/proofEngineTypes.ml
@@ -87,11 +87,18 @@ let conclusion_pattern t =
 exception Fail of string Lazy.t
 
   (** 
-    calls the opaque tactic on the status, restoring the original 
-    universe graph if the tactic Fails
+    calls the opaque tactic on the status
   *)
 let apply_tactic t status = 
-  t status
+  let (uri,metasenv,bo,ty), gl = t status in
+  match 
+    CicRefine.pack_coercion_obj 
+      (Cic.CurrentProof ("",metasenv,bo,ty,[],[]))
+  with
+  | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> 
+      (uri,metasenv,bo,ty), gl
+  | _ -> assert false
+;;
 
   (** constraint: the returned value will always be constructed by Cic.Name **)
 type mk_fresh_name_type =
diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index 970a5e388..7a675e377 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -25,7 +25,7 @@ record PreGroup : Type ≝
  }.
 
 record isGroup (G:PreGroup) : Prop ≝
- { is_monoid: isMonoid G;
+ { is_monoid:> isMonoid G;
    inv_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (inv G);
    inv_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (inv G)
  }.
@@ -73,11 +73,11 @@ intros;
 unfold left_cancellable;
 unfold injective;
 intros (x y z);
-rewrite < (e_is_left_unit ? (is_monoid ? G));
-rewrite < (e_is_left_unit ? (is_monoid ? G) z);
+rewrite < (e_is_left_unit ? G);
+rewrite < (e_is_left_unit ? G z);
 rewrite < (inv_is_left_inverse ? G x);
-rewrite > (associative ? (is_semi_group ? (is_monoid ? G)));
-rewrite > (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite > (associative ? (is_semi_group ? ( G)));
+rewrite > (associative ? (is_semi_group ? ( G)));
 apply eq_f;
 assumption.
 qed.
@@ -90,11 +90,11 @@ unfold right_cancellable;
 unfold injective;
 simplify;fold simplify (op G); 
 intros (x y z);
-rewrite < (e_is_right_unit ? (is_monoid ? G));
-rewrite < (e_is_right_unit ? (is_monoid ? G) z);
+rewrite < (e_is_right_unit ? ( G));
+rewrite < (e_is_right_unit ? ( G) z);
 rewrite < (inv_is_right_inverse ? G x);
-rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
-rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite < (associative ? (is_semi_group ? ( G)));
+rewrite < (associative ? (is_semi_group ? ( G)));
 rewrite > H;
 reflexivity.
 qed.
@@ -128,9 +128,9 @@ theorem eq_opxy_z_to_eq_x_opzinvy:
  ∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1.
 intros;
 apply (eq_op_x_y_op_z_y_to_eq ? y);
-rewrite > (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite > (associative ? G);
 rewrite > (inv_is_left_inverse ? G);
-rewrite > (e_is_right_unit ? (is_monoid ? G));
+rewrite > (e_is_right_unit ? G);
 assumption.
 qed.
 
@@ -138,7 +138,7 @@ theorem eq_opxy_z_to_eq_y_opinvxz:
  ∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z.
 intros;
 apply (eq_op_x_y_op_x_z_to_eq ? x);
-rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite < (associative ? G);
 rewrite > (inv_is_right_inverse ? G);
 rewrite > (e_is_left_unit ? (is_monoid ? G));
 assumption.
@@ -161,9 +161,9 @@ theorem morphism_to_eq_f_1_1:
  ∀G,G'.∀f:morphism G G'.f˜1 = 1.
 intros;
 apply (eq_op_x_y_op_z_y_to_eq G' (f˜1));
-rewrite > (e_is_left_unit ? (is_monoid ? G') ?);
+rewrite > (e_is_left_unit ? G' ?);
 rewrite < (f_morph ? ? f);
-rewrite > (e_is_left_unit ? (is_monoid ? G));
+rewrite > (e_is_left_unit ? G);
 reflexivity.
 qed.
  
@@ -264,7 +264,7 @@ unfold belongs_to_subgroup in H1;
 elim H1;
 clear H1;
 exists;
-[
+[apply ((a \sub H)\sup-1 · x1)
 | 
 ].
 qed.
diff --git a/helm/software/matita/library/algebra/monoids.ma b/helm/software/matita/library/algebra/monoids.ma
index c3f3cc48e..fc6c8f956 100644
--- a/helm/software/matita/library/algebra/monoids.ma
+++ b/helm/software/matita/library/algebra/monoids.ma
@@ -26,7 +26,7 @@ interpretation "premonoid magma coercion" 'pmmagma M =
  (cic:/matita/algebra/monoids/magma.con M).
 
 record isMonoid (M:PreMonoid) : Prop ≝
- { is_semi_group: isSemiGroup M;
+ { is_semi_group:> isSemiGroup M;
    e_is_left_unit:
     is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
    e_is_right_unit:
diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 07f7f900a..d498f2ab6 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -141,6 +141,17 @@ let _ =
             (UriManager.name_of_uri u ^ ":"
              ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
         (CoercDb.to_list ()));
+    addDebugItem "show coercions graph" (fun _ ->
+      let str = CoercGraph.generate_dot_file () in
+      let filename, oc = Filename.open_temp_file "xx" ".dot" in
+      output_string oc str;
+      close_out oc;
+      let ps = Filename.temp_file "yy" ".png" in
+      ignore (Sys.command ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename));
+      ignore (Sys.command ("/usr/bin/display " ^ ps));
+      Sys.remove ps;
+      Sys.remove filename);
+        
     addDebugItem "print top-level grammar entries"
       CicNotationParser.print_l2_pattern;
     addDebugItem "dump moo to stderr" (fun _ ->
diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 322fcbf41..b8c950549 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -417,7 +417,7 @@ class script  ~(source_view: GSourceView.source_view)
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
-let initial_statuses =
+let initial_statuses () =
  (* these include_paths are used only to load the initial notation *)
  let include_paths =
   Helm_registry.get_list Helm_registry.string "matita.includes" in
@@ -458,7 +458,7 @@ object (self)
 
   val mutable statements = []    (** executed statements *)
 
-  val mutable history = [ initial_statuses ]
+  val mutable history = [ initial_statuses () ]
     (** list of states before having executed statements. Head element of this
       * list is the current state, last element is the state at the beginning of
       * the script.
@@ -648,7 +648,7 @@ object (self)
 
   method private reset_buffer = 
     statements <- [];
-    history <- [ initial_statuses ];
+    history <- [ initial_statuses () ];
     userGoal <- None;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
diff --git a/helm/software/matita/scripts/crontab.sh b/helm/software/matita/scripts/crontab.sh
index 5ad50de5e..65578a87c 100644
--- a/helm/software/matita/scripts/crontab.sh
+++ b/helm/software/matita/scripts/crontab.sh
@@ -14,7 +14,7 @@ mkdir -p $TMPDIRNAME
 rm -rf $TMPDIRNAMEOLD
 cd $TMPDIRNAME
 rm -rf helm
-svn co ${SVNROOT}helm/matita/scripts/ > LOG.svn 2>&1
+svn co ${SVNROOT}helm/software/matita/scripts/ > LOG.svn 2>&1
 scripts/profile_svn.sh 2> LOG
 
 MARK=`echo "select distinct mark from bench where mark like '$TODAY%' order by mark" | mysql -u helm matita | tail -n 1`