aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofs.mllib
Commit message (Expand)AuthorAge
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
* [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
* [proof] Move bullets to their own module.Gravatar Emilio Jesus Gallego Arias2017-06-12
* proofs/proofs.mllib: no more proof_errors !Gravatar Pierre Letouzey2016-06-08
* Moving Proofview to pretyping/.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Tactic_debug to tactics/ folder.Gravatar Pierre-Marie Pédrot2016-03-06
* Moving Ltac traces to Tacexpr and Tacinterp.Gravatar Pierre-Marie Pédrot2016-03-06
* Moving Proofview_monad to the engine/ folder.Gravatar Pierre-Marie Pédrot2015-02-28
* Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Adding a tactic which fails if one of the goals under focus is dependent in a...Gravatar Hugo Herbelin2014-10-13
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...Gravatar aspiwack2013-11-02
* Revised the Ltac trace mechanism so that trace breaking due toGravatar herbelin2013-02-17
* Severe reorganisation of the code of tactics in Proofview.Gravatar aspiwack2012-07-11
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20