aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/g_extraction.mlg
AgeCommit message (Expand)Author
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-23Fixing typos - Part 2JPR
2019-03-27[plugins] [extraction] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot