aboutsummaryrefslogtreecommitdiff
path: root/proofs/pfedit.mli
AgeCommit message (Expand)Author
2015-08-02Removing the generalization of the body of inductive schemes fromHugo Herbelin
2015-01-24Tentative workaround for bug #3798.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-28Proof using: call "clear" to remove from sight the vars not selectedEnrico Tassi
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-11-02Doc: solve the bad interaction between Declare Implicit Tactic and refine.aspiwack
2013-11-02Adds a new goal selector "all:".aspiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-06Fixing ocamldoc compilation.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to to...msozeau
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-09-05Remove code concerning the obsolete Set/Unset Undoletouzey
2011-04-08Applying Tom Prince's patch for build_constant_by_tactic not able toherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-05-05Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofpboutill
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:34:48 +0000