added support for "polymorphic" coercions

[helm.git] / components / library / coercDb.ml

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index 8e2c62f310ca5b14251dcaa0a72dd2f94424688e..7203f3647e6eefb642c5fd93be6ff7d465918aa5 100644 (file)
--- a/components/library/coercDb.ml
+++ b/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