X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.ml;h=8b7982ea0576645c531fc82e5c599633ffcf39b2;hb=894802b5e169f37e5390683b6b29b4fbb4be1083;hp=8e2c62f310ca5b14251dcaa0a72dd2f94424688e;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 8e2c62f31..8b7982ea0 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -32,25 +32,26 @@ exception EqCarrOnNonMetaClosed
 let db = ref []
 
 let coerc_carr_of_term t =
-  try
-    Uri (CicUtil.uri_of_term t)
-  with Invalid_argument _ ->
-    match t with
-    | Cic.Sort s -> Sort s
-    | Cic.Appl ((Cic.Const (uri, _))::_) 
-    | Cic.Appl ((Cic.MutInd (uri, _, _))::_) 
-    | Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_) -> Uri uri
-    | t -> Term t
+ try
+  match t with
+     Cic.Sort s -> Sort s
+   | Cic.Appl (t::_)
+   | t -> Uri (CicUtil.uri_of_term t)
+ with Invalid_argument _ ->
+  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
@@ -58,12 +59,14 @@ let eq_carr src tgt =
   | Sort (Cic.Type _), Sort (Cic.Type _) -> true
   | Sort src, Sort tgt when src = tgt -> true
   | Term t1, Term t2 ->
-    if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
-      raise 
-        (EqCarrNotImplemented 
+      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
+          CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
+      else raise EqCarrOnNonMetaClosed
   | _, _ -> false
 
 let to_list () =