search

DeepSpec / InteractionTrees

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

Remove the use of "pinversion". #53

Closed gilhur closed 5 years ago

gilhur commented 5 years ago

The proof using "pinversion" was not stable (ie, breaks down with Paco 2.0.2). So, I made it more stable using "pclearbot" and "punfold" with "inv".