1. Peter Sewell
  2. lem
  3. Issues
Issue #32 resolved

Inductives naming in Coq backend

Robin Morisset
created an issue

Each case in an inductive definition is given a unique identifier, so for example we have:

Inductive ssmachine_multitrans: ... :=
  | ssmachine_multitrans_x786: ...
  | ssmachine_multitrans_x787: ...

This works, but it would be better if the counter was reset to 0 for each inductive definition, not only for readability, but also for forward compatibility (if a case is added or deleted, it would currently breaks every proof using inductives in the same file).