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 rec name_of_carr = function
| 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 () =