Adds a new unverified pass to reorder constructors (and hence the branches of cases as well). This allows to map Coq inductives to existing target language types more faithfully. For example in coq-malfunction we can map Coq's booleans (true | false naturally represented as Int(0) and Int(1)) to OCaml's booleans (false | true, represented as Int(0) and Int(1)), simplifying greatly writing correct FFIs for functions using booleans.
Adds a new unverified pass to reorder constructors (and hence the branches of cases as well). This allows to map Coq inductives to existing target language types more faithfully. For example in coq-malfunction we can map Coq's booleans (true | false naturally represented as Int(0) and Int(1)) to OCaml's booleans (false | true, represented as Int(0) and Int(1)), simplifying greatly writing correct FFIs for functions using booleans.