- let src_noxpointer = UriManager.strip_xpointer src in
- if exact && coarse_eq && UriManager.uri_is_ind src_noxpointer then
- match
- fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph src_noxpointer)
- with
- | Cic.InductiveDefinition (_,[],m,_) when m = 0 -> true
- | Cic.Constant _ -> true
- | _ -> false
- else
- coarse_eq
+ let t = CicUtil.term_of_uri src in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
+ (match ty, exact with
+ | Cic.Prod _, true -> false
+ | Cic.Prod _, false -> coarse_eq
+ | _ -> coarse_eq)