aboutsummaryrefslogtreecommitdiff
path: root/proofs/pfedit.ml
AgeCommit message (Expand)Author
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-01Cancel the start of a proof if its init_tac fails (fix #2799)letouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-05-29Pfedit: two superfluous openletouzey
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-21Pfedit: avoid Undoing too muchletouzey
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-05-13The modules in proofs now use the Errors module to explain their exceptions t...aspiwack
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
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-05-10Fix: Pfedit.get_current_goal_context when no goal is focused.aspiwack
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
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
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-01-04Fixed bugs #2001 (search_guard was overwriting the guard index givenherbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-02-22Merge with lmamane's private branch:lmamane
2006-09-20Declarative Proof Language: main commitcorbinea
2005-04-20Implementation of a new backtracking system, that allow to go backcoq
2004-12-31Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...herbelin
2004-11-18Code mortherbelin
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-07-16Nouvelle en-têteherbelin
2004-03-29Export du type de preuve en cours pour xmlherbelin
2003-10-10Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...herbelin
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...herbelin
2003-09-12open superfluherbelin
2003-01-31Pour satisfaire ProofGeneralcoq
2002-12-12Ajout du vernac Proof withgregoire
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-13simplification common_ancestorcourant
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-24Ajout d'un point d'entree pour exporter les arbres de preuves en XMLherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-04-03changement de l'undo limitbarras
2001-12-13compat ocaml 3.03filliatr
2001-11-29nouvel algo de conversion plus uniformebarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:05:08 +0000