search

imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

Name collision for path_last #5

Closed palmskog closed 6 years ago

palmskog commented 6 years ago

Both finmap/ordtype.v and pcm/heap.v have a lemma called path_last, with different meanings. This causes the importing order of files to matter, and proofs to break when the importing order is changed. Any chance the lemma in pcm/heap.v could get a different name?

anton-trunov commented 6 years ago

Thanks for reporting this! I should be able to fix it the next week.

anton-trunov commented 6 years ago

@palmskog Hi Karl, I hope this fixes the issue, so I'm closing it for now. Feel free to reopen if something goes wrong for you.