let compare = Pervasives.compare
end
module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
+module TI = Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(S)
type universe = TI.t
let empty = TI.empty
let rec dummies_of_coercions =
function
- | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
+ | Cic.Appl (c::l) when CoercDb.is_a_coercion c <> None ->
Cic.Meta (-1,[])
| Cic.Appl l ->
let l' = List.map dummies_of_coercions l in Cic.Appl l'