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