search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

Detect compspecs mismatch in SEP_field_at_unify' #681

Closed andrew-appel closed 1 year ago

andrew-appel commented 1 year ago

This fixes a bug: during forward (load_tac), if the compspecs in the field_at did not match the current compspecs, Coq could to into a unification freeze. Now if the compspecs are not constr_eq, you get an error message suggesting change_compspecs.

andrew-appel commented 1 year ago

In addition, change_compspecs itself now gives a clear diagnostic message about type mismatches, rather than freezing.