Mercurial > cpdt > repo

diff src/GeneralRec.v @ 568:81d63d9c1cc5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port to Coq 8.9.0
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:16:29 -0500
parents af97676583f3
children a913f19955e2
line wrap: on
line diff
--- a/src/GeneralRec.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/GeneralRec.v	Sun Jan 20 15:16:29 2019 -0500
@@ -654,7 +654,7 @@
        end.
 
   Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2.
-    cofix; intros;
+    cofix thunk_eq_coind; intros;
       match goal with
         | [ H' : P _ _ |- _ ] => specialize (H H'); clear H'
       end; destruct m1; destruct m2; subst; repeat constructor; auto.