CicPp.ppterm (Cic.Sort s1) ^ " <> " ^
CicPp.ppterm (Cic.Sort s2)); false)
| _ ->
+ let ty', _ =
+ CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
+ CicUniv.oblivion_ugraph
+ in
+ if CicUtil.alpha_equivalence ty ty' then
(HLog.warn
("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
"it is a duplicate of " ^ UriManager.string_of_uri u);
- true))
+ true)
+ else false
+
+ )
ul)
- (CoercDb.to_list ())
+ (CoercDb.to_list (CoercDb.dump ()))
in
let cpos = no_args - arity - saturations - 1 in
if not add_composites then