aboutsummaryrefslogtreecommitdiff
path: root/src/g_ltac2.mlg
AgeCommit message (Expand)Author
2019-04-04Adapt to coq/coq#8764Pierre Roux
2019-03-31[coq] Adapt to coq/coq#9815Pierre Roux
2019-03-31overlay for PR 9733Enrico Tassi
2019-03-20[coq] Adapt to coq/coq#9129 "removal of imperative proof state"Emilio Jesus Gallego Arias
2019-02-20[coq] Fix OCaml warnings.Emilio Jesus Gallego Arias
2019-02-08Remove VtUnknown classificationMaxime Dénès
2019-01-17Adapt to Coq's new proof mode APIMaxime Dénès
2018-12-10[coq] Adapt to coq/coq#9172Emilio Jesus Gallego Arias
2018-11-23Fix w.r.t. coq/coq#9051.Pierre-Marie Pédrot
2018-11-19Merge remote-tracking branch 'origin/pr/84'Pierre-Marie Pédrot
2018-11-19Adding a module to manipulate Ltac1 values.Pierre-Marie Pédrot
2018-11-17[coq] Overlay to adapt to coq/coq#9003Emilio Jesus Gallego Arias
2018-11-13Port to coqpp.Pierre-Marie Pédrot