CoqHott / coq-forcing

A plugin for Coq that implements the call-by-name forcing translation
12 stars 3 forks source link

Porting to 8.13 #8

Open herbelin opened 3 years ago

herbelin commented 3 years ago

Hi, this PR ports the coq-forcing plugin successively to 8.7, 8.8., 8.9, 8.10, 8.11, 8.12 and 8.13. (Hoping this is not redundant work - and if so, this anyway gives an condensed example of how Coq's API evolved in the last years).

PS: I did try to be very cautious in porting. I basically ensured that it compiled.