aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/g_extraction.mlg
AgeCommit message (Expand)Author
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