search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
204 stars 51 forks source link

Cleanup #64

Closed Zdancewic closed 5 years ago

Zdancewic commented 5 years ago

Just some slight notation and commenting changes.

Zdancewic commented 5 years ago

I plan to do a bit more polishing / cleanup in Eq.v and UpToTau.v next.

YaZko commented 5 years ago

Just in case to avoid duplicating some work, be wary that the compiler branch has led to a lot of changes in Eq and UptoTau: both eq_itree and eutt have been parameterized by a relation over the return type, rather than impose equality.

Lysxia commented 5 years ago

Some of the renaming here (esp. regarding the use of _ or F suffixes) also overlaps with what took place on the imp2asm branch.

Zdancewic commented 5 years ago

Ah -- good to know. I'll hold off doing more cleanup until we merge that branch, then.

gmalecha commented 5 years ago

What is the right thing to do with this PR? Merge it into the Imp2Asm branch?

Lysxia commented 5 years ago

I believe the changes have been merged into imp2asm.