Put forward_simulation and backward_simulation in Prop instead of Type

The original presentation of forward_simulation and backward_simulation diagrams was using records containing types, relations, and properties over these.  These records had to live in Type because in Prop the projections could not be defined.

This was causing problems with proofs of statements such as

     (exists x, P x) -> forward_simulation sem1 sem2

because the exists could not be eliminated in a Type context.

This commit re-expresses the simulation diagrams as a record of properties (in Prop) and an inductive (in Prop too) that packs the record with the types and relations.  The external interface of module Smallstep is unchanged, it's only the proofs in Smallstep and Behaviors that take a slightly different shape.

0 files changed, 0 insertions, 0 deletions