• David Hauzar's avatar
    Not appending "." to names of record fields in counterexamples. · da802d43
    David Hauzar authored
    Previously, "." was automatically appended to names stored in
    model_trace label when creating variables corresponding to record
    fields in eval_match and when projecting record fields in the
    transformation intro_projections_counterexmp. Now, this is not done
    and "." must be given in model_trace label of the projection or
    record field.
    The reason is that for SPARK, character different from "." (e.g., "'"
    needs to be sometimes appended.
ident.mli 5 KB