search

mit-plv / fiat

Mostly Automated Synthesis of Correct-by-Construction Programs
http://plv.csail.mit.edu/fiat/
Other
147 stars 31 forks source link

Implicit arguments were formerly inactive in "Context". #47

Closed herbelin closed 3 years ago

herbelin commented 3 years ago

Implicit arguments in Context were discarded. Coq PR #11390 preserves them. The present PR adapts the part of fiat tested on Coq CI to the new semantics.

I removed the declaration of the implicit arguments which were discarded anyway. In particular, the PR is backwards-compatible and can be merged as soon as now.