Internal API: process_Xhl_*

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs

MIT License

320 stars 49 forks source link

Closed strub closed 11 months ago

strub commented 11 months ago

This family of functions type-check a formula w.r.t. a memory that is infered from the program logic goal.

The commit changes two things:

for prhl, its uses the same memory name as the one used in the program logic goal. (Previously, it was using mhr)
its returns the memory that has been used for the type-checking

strub commented 11 months ago

It is strange that ecPhlConseq is not affected.

Simply because conseq does not use this API. Not sure whether we want to change this in this PR.