DeepSpec / InteractionTrees

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

rutt: swapping order of constructors and couple of simplifications #220

Closed YaZko closed 2 years ago

YaZko commented 2 years ago

Minor simplifications to [rutt]:

Note: the up-to [eqit] closure is almost a duplicate of the one used to close [eutt] itself, except that this one is heterogeneous in [E]. We could generalize the latter and reuse it here to avoid some duplication.

Also fixed a bunch of warnings against 8.14, hope it doesn't break compatibility with older versions of Coq.

Lysxia commented 2 years ago

There's a missing lower bound on coq in coq-paco.dev https://github.com/coq/opam-coq-archive/pull/2002

and I've checked that it still compiles on 8.10 on my machine. I was building the wrong branch. This branch actually fails because of #[export] only being supported on hints since 8.12.

Lysxia commented 2 years ago

I'll just remove 8.10 and 8.11 from life support.

liyishuai commented 2 years ago

Need to update coq-itree.dev in opam-coq-archive accordingly.

Lysxia commented 2 years ago

Oh, right, I can do that!