[coq] API to handle Require Ast specifically

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

GNU Lesser General Public License v2.1

145 stars 31 forks source link

[coq] API to handle Require Ast specifically #642

Closed ejgallego closed 8 months ago

ejgallego commented 8 months ago

We add some convenience functions to inspect and evaluate Coq's requires specifically.

Note that we don't yet handle the attributes / control pair of the require, this is required to be fixed before merge (likely requires cut and paste from Coq code + Coq PR to export the relevant functions to do without duplication)