aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Prelude.v
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* Add transparent_abstract tacticGravatar Jason Gross2017-04-25
* Farewell decl_modeGravatar Enrico Tassi2017-03-07
* Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Update headers.Gravatar Maxime Dénès2015-01-12
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
* Updating headers.Gravatar herbelin2012-08-08
* Remove the Dp plugin.Gravatar gmelquio2012-04-17
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...Gravatar aspiwack2011-08-09
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Parsing files for numerals (+ ascii/string) moved into pluginsGravatar letouzey2009-03-27
* Better mechanism for loading initial pluginsGravatar letouzey2009-03-14
* Fix dependency bugs due to Program modules renamings.Gravatar msozeau2007-08-08
* Move Program tactics into a proper theories/ directory as they are general pu...Gravatar msozeau2007-08-07
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursGravatar herbelin2005-02-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Ordre (symbolique) des RequireGravatar herbelin2003-10-28
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...Gravatar herbelin2003-09-23
* Suppression DatatypesSyntax et PeanoSyntax qui était videsGravatar herbelin2003-09-12
* Deplacement delimiteur T dans NotationsGravatar herbelin2003-06-10
* Concentration des notations officielles dans Init/Notations; restructuration ...Gravatar herbelin2003-05-21
* Essai d'introduction d'un scope des typesGravatar herbelin2002-12-03
* Mise en place d'ensembles de notations symboliques pour nat, Z et RGravatar herbelin2002-10-13
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
* entetesGravatar filliatr2001-03-15
* fichiers prelude CoqGravatar filliatr1999-12-13