aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Expand)AuthorAge
* 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
* Correction bug #1842 + correction bug initialisation introduit dansGravatar herbelin2008-05-10
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 00:48:47 +0000