int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
- Utils.equality_sign -> Equality.equality -> int * Equality.equality
+ Equality.equality -> int * Equality.equality
val demodulation_goal :
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->