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
;;
+let 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
+
let eq_carr src tgt =
match src, tgt with
| Uri src, Uri tgt -> UriManager.eq src tgt
else raise EqCarrOnNonMetaClosed
| _, _ -> false
-let name_of_carr = function
- | Uri u -> UriManager.name_of_uri u
- | Sort s -> CicPp.ppsort s
- | Term t -> CicPp.ppterm t
-
-
let to_list () =
!db