aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/profile_ltac_tactics.mlg
AgeCommit message (Collapse)Author
2020-09-11[refman] Rename int to integerPierre Roux
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code.