make coq export of holide work again

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

Other

265 stars 35 forks source link

Closed fblanqui closed 1 year ago

fblanqui commented 1 year ago

cli/config.ml and cli/lambdapi.ml: move options specific to export to from config.ml to lambdapi.ml
add new options specific to export: --no-implicits and --use-notations
export/coq.ml: simplify and improve code for the export to work again with holide