(fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
let match_term ~(dbd:Mysql.dbd) ty =
- prerr_endline (CicPp.ppterm ty);
+(* prerr_endline (CicPp.ppterm ty); *)
let metadata = MetadataExtractor.compute ~body:None ~ty in
let constants_no =
MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
`Obj (uri,[`InHypothesis]);
]
in
- MetadataConstraints.at_least ~dbd constraints
+ MetadataConstraints.at_least ~rating:`Hits ~dbd constraints