aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofs.mllib
AgeCommit message (Expand)Author
2021-03-22Factorize goal selector handlingGaëtan Gilbert
2020-06-29Refining out the Refiner.Pierre-Marie Pédrot
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2018-12-11[api] Move reduction modules to `tactics`Emilio Jesus Gallego Arias
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
2017-07-25[api] Put modules in order in API.{mli,ml}Emilio Jesus Gallego Arias
2017-06-12[proof] Move bullets to their own module.Emilio Jesus Gallego Arias
2016-06-08proofs/proofs.mllib: no more proof_errors !Pierre Letouzey
2016-03-20Moving Proofview to pretyping/.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
2015-02-28Moving Proofview_monad to the engine/ folder.Pierre-Marie Pédrot
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2013-11-02Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...aspiwack
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2012-07-11Severe reorganisation of the code of tactics in Proofview.aspiwack
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29Tacexpr as a mli-only, the few functions there are now in Tacopsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:03:10 +0000