search

DeepSpec / InteractionTrees

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

Rename 'do' ? #38

Closed Zdancewic closed 5 years ago

Zdancewic commented 5 years ago

Currently the record that we use for the itree CoInductive uses do as the constructor name, but I was running into some issues writing tactics that look for do because it is also an Ltac keyword. Should we change do to go or something else?

(It could also be that the tactics I'm trying to write should be written in a different way, which wouldn't run into the conflict.)

gmalecha commented 5 years ago

It makes sense to rename. Let's do it.

Zdancewic commented 5 years ago

Ok -- I'll rename it to 'go' for now. I don't think that introduces any clashes.

Zdancewic commented 5 years ago

OK -- there were two different uses of do.