search

rems-project / lem

Lem semantic definition language
Other
130 stars 15 forks source link

Should file coq-lib/lem_string.v be generated or not? #11

Closed rmn30 closed 6 years ago

rmn30 commented 6 years ago

The file coq-lib/lem_string.v is checked in to git while other lem-generated coq files are not. Looking at the history of the file it looks like Dom made some (manual?) edits to it at some point in the past but these were overwritten by generated output. The question is: are the edits still relevant and if so should we prevent lem from overwritting this file?

bacam commented 6 years ago

We should remove the generated file, because 5ec58c483242851b2a8d1289ffb953074b34920e changed the relevant Lem definition so that it doesn't need a measure in Coq. I'll double check this and commit shortly.