Fix Constructor order from extraction to fit Coq's order

jscert / jsexplain

Apache License 2.0

26 stars 4 forks source link

Fix Constructor order from extraction to fit Coq's order #46

Open barockobamo opened 5 years ago

barockobamo commented 5 years ago

From #26 :

Coq extraction has generated cases in the order of the definition of the constructors in the inductive definition; this is not the same order as in the original coq files; we should put back in the right order, i'm afraid we need to do this by hand.

IgnoredAmbience commented 5 years ago

I'm not sure we should aim for the same order as in the Coq code. A better ordering would be the same as in the ecma262 spec.