aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Prelude.v
AgeCommit message (Expand)Author
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-05-09Add hexadecimal numeralsPierre Roux
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-08-31Decimal: scope name changed dec_(u)int_scopePierre Letouzey
2018-08-31Numeral Notation for natPierre Letouzey
2018-08-31Numeral Notation: allow parsing from/to Decimal.int or Decimal.uintPierre Letouzey
2018-08-31Prelude : update the comment about ML plugins loaded by InitPierre Letouzey
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20Decimal: simple representation of base-10 numbersPierre Letouzey
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-04-25Add transparent_abstract tacticJason Gross
2017-03-07Farewell decl_modeEnrico Tassi
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
2012-08-08Updating headers.herbelin
2012-04-17Remove the Dp plugin.gmelquio
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2011-08-11SearchAbout and similar: add a customizable blacklistletouzey
2011-08-09Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...aspiwack
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
2009-03-14Better mechanism for loading initial pluginsletouzey
2007-08-08Fix dependency bugs due to Program modules renamings.msozeau
2007-08-07Move Program tactics into a proper theories/ directory as they are general pu...msozeau
2006-03-17Modification des propriétés (svn:executable)notin
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
2004-07-16Nouvelle en-têteherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-10-28Ordre (symbolique) des Requireherbelin
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-12Suppression DatatypesSyntax et PeanoSyntax qui était videsherbelin
2003-06-10Deplacement delimiteur T dans Notationsherbelin
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ...herbelin
2002-12-03Essai d'introduction d'un scope des typesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:16:48 +0000