From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 Jul 2008 21:01:17 +0000 (+0000)
Subject: simplified coercDb implementation with additional info about the position of
X-Git-Tag: make_still_working~4953
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=910c252965fe17d6b5af92e4658e7d02bac82d58;p=helm.git

simplified coercDb implementation with additional info about the position of
the coerced argument. Now (C ??? x ??? y z) is printed as (x y z) when C is a
coercion and ? are implicits or saturations generated to apply the coercion to
x.

New case in unification, when there is a triangular pullback and the
coerced is not flexible an unfolding of the composed coercion is attempted.
this helps in the case:

  C ??? X ??? y ? +?+ C1 ??? (C2 ??? X ???) ??? y z

where C = C1 composed C2 but X is rigid abd conversion fails cause
x != ? and the heads are different... unfolding C helps
---

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index b1423c5ab..c8ff783c3 100644
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -561,7 +561,7 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t
           raise Not_a_proof
     | C.AAppl (id,li) ->
         (try coercion 
-           seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts
+           seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try rewrite 
            seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
@@ -885,21 +885,31 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner
           } 
   | _ -> raise NotApplicable
 
-and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts =
+and coercion seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts =
   match li with
     | ((Cic.AConst _) as he)::tl
     | ((Cic.AMutInd _) as he)::tl
     | ((Cic.AMutConstruct _) as he)::tl when 
-       CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
-       !hide_coercions ->
-        let rec last =
-         function
-            [] -> assert false
-          | [t] -> t
-          | _::tl -> last tl
+       (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+       | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl)
+       && !hide_coercions ->
+        let cpos,sats =
+          match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+          | None -> assert false
+          | Some (_,_,_,sats,cpos) -> cpos, sats
         in
-          acic2content 
-            seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+        let x = List.nth tl cpos in
+        let _,rest = 
+          try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[] 
+        in
+        if rest = [] then
+         acic2content 
+          seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+           x
+        else
+         acic2content 
+          seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+           (Cic.AAppl (id,x::rest))
     | _ -> raise NotApplicable
 
 and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index 4c98e1ad9..edb22c944 100644
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -124,34 +124,25 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t ->
-       let last_n n l =
-         let rec aux =
-          function
-             [] -> assert false
-           | [_] as l -> l,1
-           | he::tl ->
-              let (res,len) as res' = aux tl in
-               if len < n then
-                he::res,len + 1
-               else
-                res'
-         in
-          match fst (aux l) with
-             [] -> assert false
-           | [t] -> t
-           | Ast.AttributedTerm (_,(Ast.Appl l))::tl -> 
-               idref aid (Ast.Appl (l@tl))
-           | l -> idref aid (Ast.Appl l)
-       in
        (match LibraryObjects.destroy_nat t with
        | Some n -> idref aid (Ast.Num (string_of_int n, -1))
        | None ->
            let deannot_he = Deannotate.deannotate_term he in
-           if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions
-           then
-             (match CoercDb.is_a_coercion_to_funclass deannot_he with
-             | None -> idref aid (last_n 1 (List.map k tl))
-             | Some i -> idref aid (last_n (i+1) (List.map k tl)))
+           let coercion_info = CoercDb.is_a_coercion deannot_he in
+           if coercion_info <> None && !Acic2content.hide_coercions then
+             match coercion_info with
+             | None -> assert false 
+             | Some (_,_,_,sats,cpos) -> 
+                 if cpos < List.length tl then
+                   let _,rest = 
+                     try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[] 
+                   in
+                   if rest = [] then
+                     idref aid (List.nth (List.map k tl) cpos)
+                   else
+                     idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest)))
+                 else
+                   idref aid (Ast.Appl (List.map k tl))
            else
              idref aid (Ast.Appl (List.map k args)))
     | Cic.AAppl (aid,args) ->
diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 87b3f7f42..8fa6963aa 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -132,25 +132,27 @@ let exp_impl metasenv subst context =
 ;;
 
 let is_a_double_coercion t =
-  let last_of l = 
-    let rec aux acc = function
-      | x::[] -> acc,x
-      | x::tl -> aux (acc@[x]) tl
-      | [] -> assert false
-    in
-    aux [] l
+  let rec subst_nth n x l =
+    match n,l with
+    | _, [] -> []
+    | 0, _::tl -> x :: tl
+    | n, hd::tl -> hd :: subst_nth (n-1) x tl
   in
   let imp = Cic.Implicit None in
   let dummyres = false,imp, imp,imp,imp in
   match t with
-  | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
-      (match last_of tl with
-      | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
-          let sib2,head = last_of tl2 in
-          true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
-            (c2::sib2@[imp])]) 
+  | Cic.Appl l1 ->
+     (match CoercGraph.coerced_arg l1 with
+     | Some (Cic.Appl l2, pos1) -> 
+         (match CoercGraph.coerced_arg l2 with
+         | Some (x, pos2) ->
+             true, List.hd l1, List.hd l2, x,
+              Cic.Appl (subst_nth (pos1 + 1) 
+                (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
+         | _ -> dummyres)
       | _ -> dummyres)
   | _ -> dummyres
+;;
 
 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
 =
@@ -1242,12 +1244,11 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
     let fix_arity n metasenv context subst he hetype ugraph =
       let hetype = CicMetaSubst.apply_subst subst hetype in
-      let src = CoercDb.coerc_carr_of_term hetype in 
-      let tgt = CoercDb.Fun 0 in
+      let src = CoercDb.coerc_carr_of_term hetype 0 in 
+      let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
       match CoercGraph.look_for_coercion' metasenv subst context src tgt with
       | CoercGraph.NoCoercion -> []
-      | CoercGraph.NotMetaClosed 
-      | CoercGraph.NotHandled _ ->
+      | CoercGraph.NotHandled ->
          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
       | CoercGraph.SomeCoercionToTgt candidates
       | CoercGraph.SomeCoercion candidates ->
@@ -1366,11 +1367,14 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
         CoercGraph.look_for_coercion metasenv subst context infty expty
       in
       match coer with
-      | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
-          "coerce_atom_to_something fails since not meta closed"))
       | CoercGraph.NoCoercion 
-      | CoercGraph.SomeCoercionToTgt _
-      | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
+      | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
+          "coerce_atom_to_something fails since no coercions found"))
+      | CoercGraph.NotHandled when 
+          not (CicUtil.is_meta_closed infty) || 
+          not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
+          "coerce_atom_to_something fails since carriers have metas"))
+      | CoercGraph.NotHandled -> raise (RefineFailure (lazy
           "coerce_atom_to_something fails since no coercions found"))
       | CoercGraph.SomeCoercion candidates -> 
           debug_print (lazy (string_of_int (List.length candidates) ^ 
diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 517c013d4..2bcb09937 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -594,51 +594,85 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
               | UnificationFailure s
               | Uncertain s as exn -> 
                   (match l1, l2 with
-                  | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
-                     (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
-                    CoercDb.is_a_coercion' c1 && 
-                    CoercDb.is_a_coercion' c2 &&
+                  | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), 
+                     (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
+                    CoercDb.is_a_coercion cc1 <> None && 
+                    CoercDb.is_a_coercion cc2 <> None &&
                     not (UriManager.eq uri1 uri2) ->
-(*DEBUGGING ONLY:
+(*DEBUGGING ONLY: 
 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 let res =
-*)
-                     let rec look_for_first_coercion c tl =
-                      match
-                       CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
-                      with
-                         Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
-                          when CoercDb.is_a_coercion' c' ->
-                           look_for_first_coercion c' tl'
-                       | last_tl -> c,last_tl
+        *)
+                     let inner_coerced t =
+                      let t = CicMetaSubst.apply_subst subst t in
+                      let rec aux c x t =
+                        match t with
+                        | Cic.Appl l -> 
+                            (match CoercGraph.coerced_arg l with
+                            | None -> c, x
+                            | Some (t,_) -> aux (List.hd l) t t)
+                        | _ ->  c, x
+                      in
+                      aux (Cic.Implicit None) (Cic.Implicit None) t
                      in
-                      let c1,last_tl1 = look_for_first_coercion c1 tl1 in 
-                      let c2,last_tl2 = look_for_first_coercion c2 tl2 in
-                      let car1 =
-                        CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
-                      let car2 = 
-                        CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
+                      let c1,last_tl1 = inner_coerced (Cic.Appl l1) in 
+                      let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
+                      let car1, car2 =
+                        match 
+                          CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
+                        with
+                        | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
+                        | _ -> assert false
+                      in
+                      let head1_c, head2_c =
+                        match 
+                          CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
+                        with
+                        | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
+                        | _ -> assert false
+                      in
+                      let unfold uri ens args =
+                        let o, _ = 
+                          CicEnvironment.get_obj CicUniv.oblivion_ugraph uri 
+                        in
+                        assert (ens = []);
+                        match o with
+                        | Cic.Constant (_,Some bo,_,_,_) -> 
+                            CicReduction.head_beta_reduce ~delta:false
+                              (Cic.Appl (bo::args))
+                        | _ -> assert false
+                      in
                       if CoercDb.eq_carr car1 car2 then
-                       (match last_tl1,last_tl2 with
-                           C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn
-                         | C.Meta _, _
-                         | _, C.Meta _ ->
+                         match last_tl1,last_tl2 with
+                         | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
+                         | _, C.Meta _
+                         | C.Meta _, _ ->
                            let subst,metasenv,ugraph =
                             fo_unif_subst test_equality_only subst context
                              metasenv last_tl1 last_tl2 ugraph
                            in
                             fo_unif_subst test_equality_only subst context
-                             metasenv (C.Appl l1) (C.Appl l2) ugraph
-                         | _ -> raise exn)
+                             metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
+                         | _ when CoercDb.eq_carr head1_c head2_c ->
+                           let l1, l2 = 
+                               (* composite VS composition + metas avoiding
+                                * coercions not only in coerced position *)
+                               if c1 = cc1 then 
+                                 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
+                               else Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+                           in
+                            fo_unif_subst test_equality_only subst context
+                             metasenv l1 l2 ugraph
+                         | _ -> raise exn
                       else
                        let meets = 
                          CoercGraph.meets metasenv subst context car1 car2 
                        in
-                        (match meets with
+                       (match meets with
                         | [] -> raise exn
                         | (carr,metasenv,to1,to2)::xxx -> 
                           (match xxx with
-                          [] -> ()
+                          | [] -> ()
                           | (m2,_,c2,c2')::_ ->
                           let m1,_,c1,c1' = carr,metasenv,to1,to2 in
                           let unopt = 
@@ -647,10 +681,10 @@ let res =
                           in
                           HLog.warn 
                             ("There are two minimal joins of "^
-                            CoercDb.name_of_carr car1^" and "^
-                            CoercDb.name_of_carr car2^": " ^ 
-                            CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
-                            unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+                            CoercDb.string_of_carr car1^" and "^
+                            CoercDb.string_of_carr car2^": " ^ 
+                            CoercDb.string_of_carr m1 ^ " via "^unopt c1^" + "^
+                            unopt c1'^" and "^CoercDb.string_of_carr m2^" via "^
                             unopt c2^" + "^unopt c2'));
                           let last_tl1',(subst,metasenv,ugraph) =
                            match last_tl1,to1 with
@@ -683,6 +717,7 @@ let subst,metasenv,ugraph = res in
 prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 res
 *)
+
                   (*CSC: This is necessary because of the "elim H" tactic
                          where the type of H is only reducible to an
                          inductive type. This could be extended from inductive
diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index ac7441a4c..637944e6b 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -34,22 +34,26 @@ type coercion_search_result =
   | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
   | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
   | NoCoercion
-  | NotMetaClosed
-  | NotHandled of string Lazy.t
+  | NotHandled
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 let saturate_coercion ul metasenv subst context =
   let cl =
-   List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
-  let funclass_arityl = 
-    let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in
-    List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+   List.map 
+     (fun u,saturations -> 
+        let t = CicUtil.term_of_uri u in 
+        let arity = 
+          match CoercDb.is_a_coercion t with
+          | Some (_,CoercDb.Fun i,_,_,_) -> i
+          | _ -> 0
+        in
+        arity,t,saturations) ul
   in
   let freshmeta = CicMkImplicit.new_meta metasenv subst in
-   List.map2
-    (fun arity (c,saturations) -> 
+   List.map
+    (fun (arity,c,saturations) -> 
       let ty,_ =
        CicTypeChecker.type_of_aux' ~subst metasenv context c
         CicUniv.oblivion_ugraph in
@@ -62,27 +66,29 @@ let saturate_coercion ul metasenv subst context =
         match args with
            [] -> c
          | _ -> Cic.Appl (c::args)
-    ) funclass_arityl cl
+    ) cl
 ;;
           
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion' metasenv subst context src tgt =
+  let is_dead = function CoercDb.Dead -> true | _ -> false in
   let pp_l s l =
    match l with
    | [] -> 
        debug_print 
          (lazy 
          (sprintf ":-( coercion non trovata[%s] da %s a %s" s
-             (CoercDb.name_of_carr src) 
-             (CoercDb.name_of_carr tgt)));
+             (CoercDb.string_of_carr src) 
+             (CoercDb.string_of_carr tgt)));
    | _::_ -> 
        debug_print (lazy (
                sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
            (List.length l)
-           (CoercDb.name_of_carr src) 
-           (CoercDb.name_of_carr tgt)));
+           (CoercDb.string_of_carr src) 
+           (CoercDb.string_of_carr tgt)));
   in
-  try 
+  if is_dead src || is_dead tgt then NotHandled
+  else
     let l = 
       CoercDb.find_coercion 
         (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) 
@@ -97,23 +103,23 @@ let look_for_coercion' metasenv subst context src tgt =
          pp_l "approx" l;
          (match l with
          | [] -> NoCoercion
-         | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+         | ul -> 
+            SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
      | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
-  with
-    | CoercDb.EqCarrNotImplemented s -> NotHandled s
-    | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
 ;;
 
 let look_for_coercion metasenv subst context src tgt = 
-  let src_uri = CoercDb.coerc_carr_of_term src in
-  let tgt_uri = CoercDb.coerc_carr_of_term tgt in
+  let src_uri = CoercDb.coerc_carr_of_term src 0 in
+  let tgt_uri = CoercDb.coerc_carr_of_term tgt 0 in
   look_for_coercion' metasenv subst context src_uri tgt_uri
 
 let source_of t = 
-  try
-    let uri = CicUtil.uri_of_term t in
-    CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
-  with Invalid_argument _ -> assert false (* t must be a coercion *)
+  match CoercDb.is_a_coercion t with
+  | None -> assert false
+  | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s
+  | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u
+  | Some _ -> assert false (* t must be a coercion not to funclass *)
+;;
 
 let generate_dot_file () =
   let module Pp = GraphvizPp.Dot in
@@ -123,19 +129,20 @@ let generate_dot_file () =
     ~edge_attrs:["fontsize", "10"] fmt;
   let l = CoercDb.to_list () in
   let pp_description carr =
-    match CoercDb.uri_of_carr carr with
-    | None -> ()
-    | Some uri ->
-        Pp.node (CoercDb.name_of_carr carr)
-          ~attrs:["href", UriManager.string_of_uri uri] fmt in
+    match carr with
+    | CoercDb.Uri uri ->
+        Pp.node (CoercDb.string_of_carr carr)
+          ~attrs:["href", UriManager.string_of_uri uri] fmt 
+    | _ -> ()
+  in
   List.iter
     (fun (src, tgt, ul) ->
-      let src_name = CoercDb.name_of_carr src in
-      let tgt_name = CoercDb.name_of_carr tgt in
+      let src_name = CoercDb.string_of_carr src in
+      let tgt_name = CoercDb.string_of_carr tgt in
       pp_description src;
       pp_description tgt;
       List.iter
-        (fun (u,saturations) ->
+        (fun (u,saturations,_) ->
           Pp.edge src_name tgt_name
             ~attrs:[ "label",
                      (UriManager.name_of_uri u ^
@@ -167,26 +174,12 @@ let is_composite t =
 
 let coerced_arg l =
   match l with
-  | [] | [_] -> assert false
-  | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+  | [] | [_] -> None
   | c::tl -> 
-     let arity = 
-       match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a 
-    in
-    (* decide a decent structure for coercion carriers so that all this stuff is
-     * useless *)
-    let pi = 
-      (* this calculation is not complete, since we have strange carriers *)
-      let rec count_pi = function
-        | Cic.Prod(_,_,t) -> 1+ (count_pi t)
-        | _ -> 0
-      in
-      let uri = CicUtil.uri_of_term c in
-      match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
-      | Cic.Constant (_, _, ty, _, _) -> count_pi ty
-      | _ -> assert false
-    in
-    try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
+     match CoercDb.is_a_coercion c with 
+     | None -> None
+     | Some (_,_,_,_,cpos) -> 
+        if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None
 ;;
 
 (************************* meet calculation stuff ********************)
@@ -207,7 +200,7 @@ let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
 
 let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
 
-let splat e l = List.map (fun x -> e, Some x) l;;
+let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;;
 
 (* : carr -> (carr * uri option) where the option is always Some *)
 let get_coercions_to carr = 
diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli
index 711a1527d..1a3be89f3 100644
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -34,8 +34,7 @@ type coercion_search_result =
   | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
   | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
   | NoCoercion
-  | NotMetaClosed
-  | NotHandled of string Lazy.t
+  | NotHandled
 
 val look_for_coercion :
   Cic.metasenv -> Cic.substitution -> Cic.context ->
@@ -54,7 +53,7 @@ val source_of: Cic.term -> Cic.term
 val generate_dot_file: unit -> string
 
 (* given the Appl contents returns the argument of the head coercion *)
-val coerced_arg: Cic.term list -> Cic.term option
+val coerced_arg: Cic.term list -> (Cic.term * int) option
 
 (* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
 val meets : 
diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 43906f8cd..679f4246f 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -455,7 +455,7 @@ type 'a eval_executable =
 type 'a eval_from_moo =
  { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
       
-let coercion_moo_statement_of (uri,arity, saturations) =
+let coercion_moo_statement_of (uri,arity, saturations,_) =
   GrafiteAst.Coercion
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
@@ -493,11 +493,11 @@ let eval_coercion status ~add_composites uri arity saturations =
    saturations (GrafiteTypes.get_baseuri status)
  in
  let moo_content = 
-   List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
+   List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds)
  in
  let status = GrafiteTypes.add_moo_content moo_content status in
   {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
-   List.map (fun u,_,_ -> u) compounds
+   List.map (fun u,_,_,_ -> u) compounds
 
 module MatitaStatus =
  struct
@@ -608,9 +608,9 @@ let add_coercions_of_record_to_moo obj lemmas status =
               in
               let is_a_coercion, arity_coercion = is_a_coercion uri in
               if is_a_coercion then
-                Some (uri, coercion_moo_statement_of (uri,arity_coercion,0))
+                Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0))
               else if is_a_wanted_coercion then
-                Some (uri, coercion_moo_statement_of (uri,arity_wanted,0))
+                Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0))
               else
                 None)
             lemmas)
diff --git a/helm/software/components/grafite_engine/grafiteSync.mli b/helm/software/components/grafite_engine/grafiteSync.mli
index f66c0e853..aa2749979 100644
--- a/helm/software/components/grafite_engine/grafiteSync.mli
+++ b/helm/software/components/grafite_engine/grafiteSync.mli
@@ -33,8 +33,8 @@ val add_coercion:
   add_composites:bool -> GrafiteTypes.status ->
   UriManager.uri -> int -> int ->
   string (* baseuri *) ->
-    GrafiteTypes.status * (UriManager.uri * int * int) list
-     (* URI, arity, saturations *)
+    GrafiteTypes.status * (UriManager.uri * int * int * int) list
+     (* URI, arity, saturations, cpos *)
 
 val time_travel: 
   present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index 638c0ce64..b45599ceb 100644
--- a/helm/software/components/library/cicCoercion.ml
+++ b/helm/software/components/library/cicCoercion.ml
@@ -29,7 +29,8 @@ let close_coercion_graph_ref = ref
  (fun _ _ _ _ _ -> [] : 
    CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
    string (* baseuri *) ->
-     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * int) list)
+     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj *
+     int * int) list)
 ;;
 
 let set_close_coercion_graph f = close_coercion_graph_ref := f;;
diff --git a/helm/software/components/library/cicCoercion.mli b/helm/software/components/library/cicCoercion.mli
index 97463b1d6..8356de8cd 100644
--- a/helm/software/components/library/cicCoercion.mli
+++ b/helm/software/components/library/cicCoercion.mli
@@ -29,12 +29,12 @@ val set_close_coercion_graph :
   (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
-      int (* saturations *) * Cic.obj * int (* arity *)) list)
+      int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list)
   -> unit
 
 val close_coercion_graph:
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
-      int (* saturations *) * Cic.obj * int (* arity *) ) list
+      int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list
 
diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 80222ad34..50db7a3c1 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -25,48 +25,47 @@
 
 (* $Id$ *)
 
+let debug = false
+let debug_print =
+  if debug then fun x -> prerr_endline (Lazy.force x)
+  else ignore
+;;
+
 type coerc_carr = 
   | Uri of UriManager.uri 
   | Sort of Cic.sort 
-  | Term of Cic.term
   | Fun of int 
+  | Dead
 ;;
 
-exception EqCarrNotImplemented of string Lazy.t
-exception EqCarrOnNonMetaClosed
+type saturations = int
+type coerced_pos = int
+type coercion_entry = 
+  coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos
+
+type coerc_db = (* coercion_entry grouped by carrier with molteplicity *)
+ (coerc_carr * coerc_carr * 
+   (UriManager.uri * int * saturations * coerced_pos) list) list
 
-let db = ref []
+let db =  ref ([] : coerc_db)
+let dump () = !db 
+let restore coerc_db = db := coerc_db
 
-let coerc_carr_of_term t =
+let rec coerc_carr_of_term t a =
  try
-  match t with
-   | Cic.Sort s -> Sort s
-   | Cic.Prod _ -> Fun 0 
-     (* BUG: this should be the real arity. The computation
-      requires menv, context etc.., but since carrs are compared discharging Fun
-      arity... it works *)
-   | Cic.Appl (t::_)
-   | t -> Uri (CicUtil.uri_of_term t)
- with Invalid_argument _ ->
-  Term t
+  match t, a with
+   | Cic.Sort s, 0 -> Sort s
+   | Cic.Appl (t::_), 0 -> coerc_carr_of_term t a
+   | t, 0 -> Uri (CicUtil.uri_of_term t)
+   | _, n -> Fun n
+ with Invalid_argument _ -> Dead
 ;;
 
-let uri_of_carr = function
-  | Uri u -> Some u
-  | _ -> None
-
-let rec name_of_carr = function
+let string_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 (Cic.Prod (_,_,t)) -> name_of_carr (Term t)
-  | Term t -> 
-      prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t); 
-      "FixTheNameMangler"
   | Fun i -> "FunClass_" ^ string_of_int i   
+  | Dead -> "UnsupportedCarrier"
 ;;
 
 let eq_carr ?(exact=false) src tgt =
@@ -81,24 +80,13 @@ let eq_carr ?(exact=false) src tgt =
       | _ -> coarse_eq) 
   | Sort (Cic.Type _), Sort (Cic.Type _) -> true
   | Sort src, Sort tgt when src = tgt -> true
-  | Term t1, Term t2 ->
-      if t1 = t2 then true
-      else
-        if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
-          raise 
-          (EqCarrNotImplemented 
-          (lazy ("Unsupported carr for coercions: " ^ 
-          CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
-      else raise EqCarrOnNonMetaClosed
-  | Fun _,Fun _ -> true (* only one Funclass? *)
-(*   | Fun i,Fun j when i=j -> true *)
-  | Term t, _
-  | _, Term t when not (CicUtil.is_meta_closed t) -> raise EqCarrOnNonMetaClosed
+  | Fun _,Fun _ when not exact -> true (* only one Funclass *)
+  | Fun i,Fun j when i = j -> true (* only one Funclass *)
   | _, _ -> false
 ;;
 
 let to_list () =
-  List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db
+  List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) !db
 ;;
 
 let rec myfilter p = function
@@ -106,14 +94,11 @@ let rec myfilter p = function
   | (s,t,l)::tl ->
       let l = 
         HExtlib.filter_map 
-          (fun (u,n,saturations) -> 
-            if p (s,t,u,saturations) then
-              if n = 1 then
-                None
-              else
-                Some (u,n-1,saturations)
-            else
-              Some (u,n,saturations)) 
+          (fun (u,n,saturations,cpos) as e -> 
+            if p (s,t,u,saturations,cpos) then
+              if n = 1 then None
+              else Some (u,n-1,saturations,cpos)
+            else Some e) 
           l 
       in
       if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
@@ -122,75 +107,54 @@ let rec myfilter p = function
 let remove_coercion p = db := myfilter p !db;;
 
 let find_coercion f =
-    List.map
-    (fun uri,_,saturations -> uri,saturations)
-    (List.flatten
+  List.map
+   (fun (uri,_,saturations,_) -> uri,saturations)
+   (List.flatten
     (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
 ;;
 
-let get_carr uri =
+let is_a_coercion t = 
   try
-    let src, tgt, _ = 
-      List.find 
-        (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq uri x) xl) 
-        !db 
-    in
-    src, tgt
-  with Not_found -> assert false (* uri must be a coercion *)
+   let uri = CicUtil.uri_of_term t in
+   match 
+     HExtlib.filter_map
+      (fun (src,tgt,xl) -> 
+         let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in
+         if xl = [] then None else Some (src,tgt,xl))
+      !db
+   with
+   | [] -> None
+   | (_,_,[])::_ -> assert false
+   | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p)
+   | (src,tgt,(u,_,s,p)::_)::_ -> 
+       debug_print 
+         (lazy "coercion has multiple entries, returning the first one");
+       Some (src,tgt,u,s,p)
+  with Invalid_argument _ -> 
+    debug_print (lazy "this term is not a constant");      
+    None
 ;;
 
-let is_a_coercion u = 
-  List.exists 
-    (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq u x) xl) 
-    !db
-;;
-
-let is_a_coercion' t = 
-  try
-    let uri = CicUtil.uri_of_term t in
-     is_a_coercion uri
-  with Invalid_argument _ -> false
-;;
-
-let is_a_coercion_to_funclass t =
-  try
-    let uri = CicUtil.uri_of_term t in
-    match snd (get_carr uri) with
-    | Fun i -> Some i
-    | _ -> None
-  with Invalid_argument _ -> None
-  
-
-let term_of_carr = function
-  | Uri u -> CicUtil.term_of_uri u
-  | Sort s -> Cic.Sort s
-  | Fun _ -> assert false
-  | Term _ -> assert false
-;;
-  
-let add_coercion (src,tgt,u,saturations) =
+let add_coercion (src,tgt,u,saturations,cpos) =
   let f s t = eq_carr s src && eq_carr t tgt in
   let where = List.filter (fun (s,t,_) -> f s t) !db in
   let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
   match where with
-  | [] -> db := (src,tgt,[u,1,saturations]) :: !db
+  | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !db
   | (src,tgt,l)::tl ->
       assert (tl = []); (* not sure, this may be a feature *)
-      if List.exists (fun (x,_,_) -> UriManager.eq u x) l then
-        let l' = List.map
-          (fun (x,n,saturations') ->
+      if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then
+        let l = List.map
+          (fun (x,n,x_saturations,x_cpos) as e ->
             if UriManager.eq u x then
-             (x,n+1,saturations)
-            else
-             (x,n,saturations))
+             (* not sure, this may be a feature *)
+             (assert (x_saturations = saturations && x_cpos = cpos);       
+             (x,n+1,saturations,cpos))
+            else e)
           l
         in
-        db := (src,tgt,l')::tl @ rest
+        db := (src,tgt,l)::tl @ rest
       else
-        db := (src,tgt,(u,1,saturations)::l)::tl @ rest
-      
+        db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest
 ;;
 
-type coerc_db = (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list 
-let dump () = !db 
-let restore coerc_db = db := coerc_db
diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli
index 3071aecc4..130987df8 100644
--- a/helm/software/components/library/coercDb.mli
+++ b/helm/software/components/library/coercDb.mli
@@ -24,49 +24,41 @@
  *)
 
 
- (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph/CicCoercion/librarySync
-  * 
-  *   and may be merged with CicCoercion...
-  *  
-  * **)
-
-
-  (** XXX WARNING: non-reentrant *)
-type coerc_carr = 
+type coerc_carr = private 
   | Uri of UriManager.uri (* const, mutind, mutconstr *)
   | Sort of Cic.sort (* Prop, Set, Type *) 
-  | Term of Cic.term (* nothing supported *)
   | Fun of int
+  | Dead
 ;;
   
-exception EqCarrNotImplemented of string Lazy.t
-exception EqCarrOnNonMetaClosed
 val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool
-val coerc_carr_of_term: Cic.term -> coerc_carr
-val name_of_carr: coerc_carr -> string
-val uri_of_carr: coerc_carr -> UriManager.uri option
+val string_of_carr: coerc_carr -> string
+
+(* takes a term in whnf ~delta:false and a desired ariety *)
+val coerc_carr_of_term: Cic.term -> int -> coerc_carr 
 
 val to_list:
   unit -> 
-    (coerc_carr * coerc_carr * (UriManager.uri * int) list) list
+    (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
 
 type coerc_db
 val dump: unit -> coerc_db
 val restore: coerc_db -> unit
 
-val add_coercion:
-  coerc_carr * coerc_carr * UriManager.uri * int -> unit
+(* src carr, tgt carr, uri, saturations, coerced position 
+ * invariant:
+ *   if the constant pointed by uri has n argments
+ *   n = coerced position + saturations + FunClass arity
+ *)
 
-val remove_coercion:
-  (coerc_carr * coerc_carr * UriManager.uri * int -> bool) -> unit
+type saturations = int
+type coerced_pos = int
+type coercion_entry = 
+  coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos
+val add_coercion: coercion_entry -> unit
+val remove_coercion: (coercion_entry -> bool) -> unit
 
 val find_coercion: 
   (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list 
     
-val is_a_coercion: UriManager.uri -> bool
-val is_a_coercion': Cic.term -> bool
-val is_a_coercion_to_funclass: Cic.term -> int option
-val get_carr: UriManager.uri -> coerc_carr * coerc_carr
-
-val term_of_carr: coerc_carr -> Cic.term
-
+val is_a_coercion: Cic.term -> coercion_entry option
diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 4b85d61bc..13596c84e 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -138,12 +138,9 @@ let index_obj =
 let add_single_obj uri obj refinement_toolkit =
   let module RT = RefinementTool in
   let obj = 
-    if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
-       not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
-    then
-      refinement_toolkit.RT.pack_coercion_obj obj
-    else
-      obj 
+    if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None
+    then refinement_toolkit.RT.pack_coercion_obj obj
+    else obj 
   in
   let dbd = LibraryDb.instance () in
   if CicEnvironment.in_library uri then
@@ -244,7 +241,7 @@ let generate_elimination_principles uri refinement_toolkit =
   
 let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
-  CoercDb.remove_coercion (fun (_,_,_,_) -> true)
+  CoercDb.remove_coercion (fun _ -> true)
 
 let stack = ref [];;
 
@@ -294,7 +291,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     in
     aux ty
   in
-  let src_carr, tgt_carr = 
+  let src_carr, tgt_carr, no_args = 
     let get_classes arity saturations l = 
       (* this is the ackerman's function revisited *)
       let rec aux = function
@@ -312,18 +309,19 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     in
     let types = spine2list coer_ty in
     let src,tgt = get_classes arity saturations types in
-     CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
-     match tgt with
-        None -> assert false
-      | Some `Funclass -> CoercDb.Fun arity
-      | Some (`Class tgt) ->
-         CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+     CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
+     (match tgt with
+     | None -> assert false
+     | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
+     | Some (`Class tgt) ->
+         CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
+     List.length types - 1
   in
   let already_in_obj src_carr tgt_carr uri obj = 
      List.exists 
       (fun (s,t,ul) -> 
         List.exists 
-         (fun u,_ -> 
+         (fun u,_,_ -> 
            let bo = 
             match obj with 
             | Cic.Constant (_, Some bo, _, _, _) -> bo
@@ -343,8 +341,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
          ul)
       (CoercDb.to_list ())
   in
+  let cpos = no_args - arity - saturations - 1 in 
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
     UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
     [])
   else
@@ -353,22 +352,24 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        baseuri
     in
     let new_coercions = 
-      List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
+      List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
       new_coercions 
     in
-    let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
+    let composite_uris = 
+      List.map (fun (_,_,uri,_,_,_,_) -> uri) new_coercions 
+    in
     (* update the DB *)
     List.iter 
-      (fun (src,tgt,uri,saturations,_,_) ->
-        CoercDb.add_coercion (src,tgt,uri,saturations)) 
+      (fun (src,tgt,uri,saturations,_,_,cpos) ->
+        CoercDb.add_coercion (src,tgt,uri,saturations,cpos)) 
       new_coercions;
-    CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
     (* add the composites obj and they eventual lemmas *)
     let lemmas = 
         List.fold_left
-          (fun acc (_,tgt,uri,saturations,obj,arity) -> 
+          (fun acc (_,tgt,uri,saturations,obj,arity,cpos) -> 
             add_single_obj uri obj refinement_toolkit;
-             (uri,arity,saturations)::acc) 
+             (uri,arity,saturations,cpos)::acc) 
           [] new_coercions
     in
     (* store that composite_uris are related to uri. the first component is
@@ -399,10 +400,11 @@ let remove_coercion uri =
       composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
     CoercDb.remove_coercion 
-      (fun (_,_,u,_) -> UriManager.eq uri u);
+      (fun (_,_,u,_,_) -> UriManager.eq uri u);
     (* remove from the DB *) 
     List.iter 
-      (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
+      (fun u -> 
+         CoercDb.remove_coercion (fun (_,_,u1,_,_) -> UriManager.eq u u1))
       composites_in_db;
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
@@ -442,7 +444,7 @@ let generate_projections refinement_toolkit uri fields =
   prerr_endline "---";
 *)
               (*CSC: I throw the arity away. See comment above *)
-              List.map (fun u,_,_ -> u) x
+              List.map (fun u,_,_,_ -> u) x
             end
           else  
             []
diff --git a/helm/software/components/library/librarySync.mli b/helm/software/components/library/librarySync.mli
index 9dd3f5c3c..13a6479bd 100644
--- a/helm/software/components/library/librarySync.mli
+++ b/helm/software/components/library/librarySync.mli
@@ -51,7 +51,7 @@ val add_coercion:
   add_composites:bool -> 
   RefinementTool.kit -> UriManager.uri -> int (* arity *) ->
    int (* saturations *) -> string (* baseuri *) ->
-    (UriManager.uri * int * int) list (* URI, arity, saturations *)
+    (UriManager.uri * int * int * int) list (* URI, arity, saturations, cpos *)
 
 (* inverse of add_coercion, removes both the eventually created composite   *)
 (* coercions and the information that [uri] and the composites are coercion *)
diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index e9a123ad8..0041685ef 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -33,39 +33,32 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  * (source, list of coercions to follow, target)
  *)
 let get_closure_coercions src tgt uri coercions =
-  let enrich (uri,sat) tgt =
+  let enrich (uri,sat,_) tgt =
    let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
     uri,sat,arity
   in
   let uri = enrich uri tgt in
   let eq_carr ?exact s t = 
-    debug_print (lazy(CoercDb.name_of_carr s^" VS "^CoercDb.name_of_carr t));
-    try
-            let rc = CoercDb.eq_carr ?exact s t in
-            debug_print(lazy(string_of_bool rc));
-            rc
-    with
-    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> 
-        debug_print (lazy("false"));            
-        false
+    debug_print(lazy(CoercDb.string_of_carr s^" VS "^CoercDb.string_of_carr t));
+    let rc = CoercDb.eq_carr ?exact s t in
+    debug_print(lazy(string_of_bool rc));
+    rc
   in
   match src,tgt with
   | CoercDb.Uri _, CoercDb.Uri _ ->
-                  debug_print (lazy ("Uri, Uri4"));
+      debug_print (lazy ("Uri, Uri4"));
       let c_from_tgt = 
         List.filter 
           (fun (f,t,_) -> 
-                  
-                  debug_print (lazy ("Uri, Uri3"));
-                  eq_carr f tgt (*&& not (eq_carr t src)*)) 
+             debug_print (lazy ("Uri, Uri3"));
+             eq_carr f tgt) 
           coercions 
       in
       let c_to_src = 
         List.filter 
           (fun (f,t,_) -> 
-                  
-                  debug_print (lazy ("Uri, Uri2"));
-                  eq_carr t src (*&& not (eq_carr f tgt)*)) 
+             debug_print (lazy ("Uri, Uri2"));
+             eq_carr t src) 
           coercions 
       in
         (HExtlib.flatten_map 
@@ -249,9 +242,9 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       | (i,_,_)::_ when i = n -> acc
       | _::tl -> position_of n (acc + 1) tl
     in
-    let saturations_res = 
+    let saturations_res, position_of_meta_to_be_coerced = 
       match meta_to_be_coerced with
-      | None -> 0
+      | None -> 0,0
       | Some meta_to_be_coerced -> 
           debug_print
             (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced));
@@ -259,10 +252,11 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
             position_of meta_to_be_coerced 0 sorted in
           debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^
             string_of_int position_of_meta_to_be_coerced));
-          List.length sorted - position_of_meta_to_be_coerced - 1
+          List.length sorted - position_of_meta_to_be_coerced - 1,
+          position_of_meta_to_be_coerced
     in
     debug_print (lazy ("SATURATIONS: " ^ string_of_int saturations_res));
-    sorted, saturations_res
+    sorted, saturations_res, position_of_meta_to_be_coerced
   in
   let namer l n = 
     let l = List.map (function Cic.Name s -> s | _ -> "A") l in
@@ -287,7 +281,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
   let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in
   debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
   let old_insert_coercions = !CicRefine.insert_coercions in
-  let c, metasenv, univ, saturationsres =
+  let c, metasenv, univ, saturationsres, cpos =
     try
       CicRefine.insert_coercions := false;
       let term, ty, metasenv, ugraph = 
@@ -303,7 +297,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       in
       debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
       debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv));
-      let body_metasenv, saturationsres =
+      let body_metasenv, saturationsres, cpos =
        order_body_menv term body_metasenv c1_pis c2_pis
       in
       debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
@@ -340,7 +334,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       debug_print (lazy ("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
       debug_print (lazy ("####################"));
       CicRefine.insert_coercions := old_insert_coercions;
-      term, metasenv, ugraph, saturationsres
+      term, metasenv, ugraph, saturationsres, cpos
     with
     | CicRefine.RefineFailure s 
     | CicRefine.Uncertain s -> debug_print s; 
@@ -350,7 +344,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
         CicRefine.insert_coercions := old_insert_coercions;
         raise exn
   in
-  c, metasenv, univ, saturationsres, arity2
+  c, metasenv, univ, saturationsres, arity2, cpos
 ;;
 
 let build_obj c univ arity =
@@ -372,16 +366,18 @@ let build_obj c univ arity =
 (* removes from l the coercions that are in !coercions *)
 let filter_duplicates l coercions =
   List.filter (
-      fun (src,l1,tgt) ->
-        not (List.exists (fun (s,t,l2) -> 
-          CoercDb.eq_carr s src && 
-          CoercDb.eq_carr t tgt &&
-          try 
-            List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
-          with
-          | Invalid_argument "List.for_all2" -> debug_print (lazy("XXX")); false)
-        coercions))
+   fun (src,l1,tgt) ->
+     not (List.exists (fun (s,t,l2) -> 
+       CoercDb.eq_carr s src && 
+       CoercDb.eq_carr t tgt &&
+       try 
+         List.for_all2 (fun (u1,_,_) (u2,_,_) -> UriManager.eq u1 u2) l1 l2
+       with
+       | Invalid_argument "List.for_all2" -> 
+           debug_print (lazy("XXX")); false)
+     coercions))
   l
+;;
 
 let mangle s t l = 
   (*List.fold_left
@@ -429,7 +425,7 @@ let number_if_already_defined buri name l =
 let close_coercion_graph src tgt uri saturations baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
-  let todo_list = get_closure_coercions src tgt (uri,saturations) coercions in
+  let todo_list = get_closure_coercions src tgt (uri,saturations,0) coercions in
   debug_print (lazy("composed " ^ string_of_int (List.length todo_list)));
   let todo_list = filter_duplicates todo_list coercions in
   try
@@ -437,47 +433,46 @@ let close_coercion_graph src tgt uri saturations baseuri =
       List.fold_left 
         (fun acc (src, l , tgt) ->
           try 
-            (match l with
+            match l with
             | [] -> assert false 
             | (he,saturations1,arity1) :: tl ->
                 let first_step = 
-                  Cic.Constant ("", 
-                   Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+                  Cic.Constant ("", Some (CicUtil.term_of_uri he),
                     Cic.Sort Cic.Prop, [], obj_attrs arity1),
                   saturations1,
-                  arity1
+                  arity1,0
                 in
                 let o,_ = 
                   List.fold_left (fun (o,univ) (coer,saturations2,arity2) ->
                     match o with 
-                    | Cic.Constant (_,Some u,_,[],_),saturations1,arity1 ->
-                        let t, menv, univ, saturationsres, arityres = 
+                    | Cic.Constant (_,Some u,_,[],_),saturations1,arity1,_ ->
+                        let t, menv, univ, saturationsres, arityres, cposres = 
                           generate_composite' (u,saturations1,arity1) 
-                            (CoercDb.term_of_carr (CoercDb.Uri coer),
+                            (CicUtil.term_of_uri coer,
                              saturations2, arity2) [] [] univ
                         in
                         if (menv = []) then
                           HLog.warn "MENV non empty after composing coercions";
                         let o,univ = build_obj t univ arityres in
-                         (o,saturationsres,arityres),univ
+                         (o,saturationsres,arityres,cposres),univ
                     | _ -> assert false 
                   ) (first_step, CicUniv.oblivion_ugraph) tl
                 in
-                let name_src = CoercDb.name_of_carr src in
-                let name_tgt = CoercDb.name_of_carr tgt in
+                let name_src = CoercDb.string_of_carr src in
+                let name_tgt = CoercDb.string_of_carr tgt in
                 let by = List.map (fun u,_,_ -> UriManager.name_of_uri u) l in
                 let name = mangle name_tgt name_src by in
                 let c_uri = 
                   number_if_already_defined baseuri name 
-                    (List.map (fun (_,_,u,_,_,_) -> u) acc) 
+                    (List.map (fun (_,_,u,_,_,_,_) -> u) acc) 
                 in
-                let named_obj,saturations,arity = 
+                let named_obj,saturations,arity,cpos = 
                   match o with
-                  | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity ->
-                      Cic.Constant (name,bo,ty,vl,attrs),saturations,arity
+                  | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity,cpos ->
+                      Cic.Constant (name,bo,ty,vl,attrs),saturations,arity,cpos
                   | _ -> assert false 
                 in
-                  (src,tgt,c_uri,saturations,named_obj,arity))::acc
+                  (src,tgt,c_uri,saturations,named_obj,arity,cpos)::acc
           with UnableToCompose -> acc
       ) [] todo_list
     in
@@ -490,7 +485,7 @@ CicCoercion.set_close_coercion_graph close_coercion_graph;;
 (* generate_composite (c2 (c1 s)) in the universe graph univ
  * both living in the same context and metasenv *)
 let generate_composite c1 c2 context metasenv univ sat1 sat2 =
- let a,b,c,_,_ =
+ let a,b,c,_,_,_ =
   generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ
  in
   a,b,c
diff --git a/helm/software/components/tactics/closeCoercionGraph.mli b/helm/software/components/tactics/closeCoercionGraph.mli
index 0d5a2e5be..70c4eff9a 100644
--- a/helm/software/components/tactics/closeCoercionGraph.mli
+++ b/helm/software/components/tactics/closeCoercionGraph.mli
@@ -29,7 +29,7 @@ val close_coercion_graph:
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
-      int (* saturations *) * Cic.obj * int (* arity *)) list
+      int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list
 
 exception UnableToCompose
 
diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index f7c3932dc..8fb710755 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -73,7 +73,7 @@ let rec collapse_head_metas t =
 
 let rec dummies_of_coercions = 
   function
-    | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
+    | Cic.Appl (c::l) when CoercDb.is_a_coercion c <> None ->
         Cic.Meta (-1,[])
     | Cic.Appl l -> 
         let l' = List.map dummies_of_coercions l in Cic.Appl l'
diff --git a/helm/software/matita/contribs/dama/dama/models/list_support.ma b/helm/software/matita/contribs/dama/dama/models/list_support.ma
index 3aec1a024..1125e2a91 100644
--- a/helm/software/matita/contribs/dama/dama/models/list_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/list_support.ma
@@ -41,10 +41,24 @@ lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.\len (\mk_list f n) = n.
 intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity;
 qed.
 
-inductive sorted (T:Type) (lt : T → T → Prop): list T → Prop ≝ 
-| sorted_nil : sorted T lt []
-| sorted_one : ∀x. sorted T lt [x]
-| sorted_cons : ∀x,y,tl. lt x y → sorted T lt (y::tl) → sorted T lt (x::y::tl). 
+record rel : Type ≝ {
+  rel_T :> Type;
+  rel_op :2> rel_T → rel_T → Prop
+}.
+
+record trans_rel : Type ≝ {
+  o_rel :> rel;
+  o_tra : ∀x,y,z: o_rel.o_rel x y → o_rel y z → o_rel x z 
+}.
+
+lemma trans: ∀r:trans_rel.∀x,y,z:r.r x y → r y z → r x z.
+apply o_tra;
+qed.
+
+inductive sorted (lt : trans_rel): list (rel_T lt) → Prop ≝ 
+| sorted_nil : sorted lt []
+| sorted_one : ∀x. sorted lt [x]
+| sorted_cons : ∀x,y,tl. lt x y → sorted lt (y::tl) → sorted lt (x::y::tl). 
 
 lemma nth_nil: ∀T,i.∀def:T. \nth [] def i = def.
 intros; elim i; simplify; [reflexivity;] assumption; qed.
@@ -61,25 +75,23 @@ lemma len_gt_non_empty :
 intros; cases l in H; [intros; cases (not_le_Sn_O ? H);] intros; constructor 1;
 qed. 
 
-lemma sorted_tail: ∀T,r,x,l.sorted T r (x::l) → sorted T r l.
+lemma sorted_tail: ∀r,x,l.sorted r (x::l) → sorted r l.
 intros; inversion H; intros; [destruct H1;|destruct H1;constructor 1;]
 destruct H4; assumption;
 qed.
 
-lemma sorted_skip: 
- ∀T,r,x,y,l. 
-  transitive T r → sorted T r (x::y::l) → sorted T r (x::l).
-intros; inversion H1; intros; [1,2: destruct H2]
-destruct H5; inversion H3; intros; [destruct H5]
-[1: destruct H5; constructor 2;
-|2: destruct H8; constructor 3; [apply (H ??? H2 H5);]
-    apply (sorted_tail ???? H3);]
+lemma sorted_skip: ∀r,x,y,l. sorted r (x::y::l) → sorted r (x::l).
+intros (r x y l H1); inversion H1; intros; [1,2: destruct H]
+destruct H4; inversion H2; intros; [destruct H4]
+[1: destruct H4; constructor 2;
+|2: destruct H7; constructor 3; [ apply (o_tra ? ??? H H4);]
+    apply (sorted_tail ??? H2);]
 qed.
 
-lemma sorted_tail_bigger : ∀T,r,x,l,d.sorted T r (x::l) → ∀i. i < \len l → r x (\nth l d i).
+lemma sorted_tail_bigger : ∀r,x,l,d.sorted r (x::l) → ∀i. i < \len l → r x (\nth l d i).
 intros 4; elim l; [ cases (not_le_Sn_O i H1);]
 cases i in H2;
-[2: intros; apply (H d ? n);[apply (sorted_skip ????? H1)|apply le_S_S_to_le; apply H2]
+[2: intros; apply (H ? n);[apply (sorted_skip ???? H1)|apply le_S_S_to_le; apply H2]
 |1: intros; inversion H1; intros; [1,2: destruct H3]
     destruct H6; simplify; assumption;]
 qed. 
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
index cb73c2d5f..220601745 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
@@ -57,7 +57,7 @@ letin m ≝ (hide ? (
         apply le_plus_n_r;] 
 |2,3: clear H6;
     cases (aux n1) in H5 ⊢ %; intros;
-    change in match (a 〈w,H5〉) in H6 ⊢ % with (a w);
+    change in match (a ≪w,H5≫) in H6 ⊢ % with (a w);
     cases H5; clear H5; cases H7; clear H7;
     [1: left; split; [ apply (le_S ?? H5); | assumption]
     |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
index 8b062b6de..dd1f52b72 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
@@ -15,13 +15,12 @@
 include "lebesgue.ma".
 include "models/nat_order_continuous.ma".
 
-alias symbol "pair" = "dependent pair".
 theorem nat_lebesgue_oc:
    ∀a:sequence ℕ.∀l,u:ℕ.∀H:∀i:nat.a i ∈ [l,u]. 
      ∀x:ℕ.a order_converges x → 
       x ∈ [l,u] ∧ 
       ∀h:x ∈ [l,u].
-       uniform_converge {[l,u]} ⌊n,〈a n,H n〉⌋ 〈x,h〉.
+       uniform_converge {[l,u]} ⌊n,≪a n,H n≫⌋ ≪x,h≫.
 intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption;
 qed.
 
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index a48eb164a..a492c8f32 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -217,7 +217,7 @@ qed.
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
    exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
-     (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
+     (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
                    (u i) is_supremum ⌊w,a (w+i)⌋).
     
 notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index c559358c5..b39eb8531 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -255,11 +255,11 @@ let _ =
           HLog.debug
            ((String.concat ","
               (List.map
-                (fun u,saturations ->
+                (fun u,saturations,_ ->
                   UriManager.name_of_uri u ^
                    "(" ^ string_of_int saturations ^ ")")
                 ul)) ^ ":"
-             ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
+             ^ CoercDb.string_of_carr s ^ " -> " ^ CoercDb.string_of_carr t))
         (CoercDb.to_list ()));
     addDebugSeparator ();
     let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in
diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml
index 312a9a4f8..076a5d763 100644
--- a/helm/software/matita/matitaExcPp.ml
+++ b/helm/software/matita/matitaExcPp.ml
@@ -145,8 +145,6 @@ let rec to_string =
      None, "Type checking assertion failed: " ^ Lazy.force msg
   | LibrarySync.AlreadyDefined s -> 
      None, "Already defined: " ^ UriManager.string_of_uri s
-  | CoercDb.EqCarrNotImplemented msg ->
-     None, ("EqCarrNotImplemented: " ^ Lazy.force msg)
   | DisambiguateChoices.Choice_not_found msg ->
      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
   | MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->