aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofs.mllib
Commit message (Expand)AuthorAge
* 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