This is only a partial overlay. The CompCert and Flocq subfolders still contain calls to casetype / elimtype, but these should go away when their version is bumped. Some other uses in VST proper were also left, since they seem to correspond to a local Ltac idiom to convey error messages to the user.
This is only a partial overlay. The CompCert and Flocq subfolders still contain calls to casetype / elimtype, but these should go away when their version is bumped. Some other uses in VST proper were also left, since they seem to correspond to a local Ltac idiom to convey error messages to the user.