Fix for Coq 8.6 - Githubissues

CoqHott / coq-forcing

A plugin for Coq that implements the call-by-name forcing translation

12 stars 3 forks source link

Fix for Coq 8.6 #1

Closed SkySkimmer closed 3 years ago

SkySkimmer commented 7 years ago

need to open things in the ml4
Context LocalAssum/LocalDef elements appeared
some name changes (Errors -> CErrors, Typing.check -> Typing.e_check, Pp.msg_info -> Feedback.msg_info)
Proofview.Goal.nf_enter takes a Sigma aware argument.

SkySkimmer commented 6 years ago

Oops, I pushed the sprop stuff to this branch. Now fixed.

herbelin commented 3 years ago

Hi, I tested @SkySkimmer's patch which worked well. What are the plans? Do you plan to release a 8.6 branch of the plugin?

I may try to port the plugin to 8.7 (it apparently requires moving some functions to EConstr)? Or are there already versions of the forcing plugin available for more recent versions of Coq (maybe based on MetaCoq?)?

Thanks in advance for help.

herbelin commented 3 years ago

Any objections to merging this PR?