aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Postpone checking of Local/Global to allow grammar extensions to use itGravatar msozeau2009-09-02
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* DISCLAIMERGravatar puech2009-01-17
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Minor improvement to commit 11619Gravatar herbelin2008-11-23
* Fixed bug #2006 (type constraint on Record was not taken into account) +Gravatar herbelin2008-11-23
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* In manual implicit arguments mode, do not enrich implicitsGravatar msozeau2008-09-14
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* Suite commit 11236Gravatar notin2008-07-24
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Affichage intempestif d'information de globalisation + numéro de version dan...Gravatar notin2008-07-18
* fixed indentation of subgoals for Show ScriptGravatar barras2008-07-17
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Suite de la révision #11212Gravatar notin2008-07-08
* Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...Gravatar notin2008-07-07
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
* Strategy commands are now exportedGravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 15:55:23 +0000