aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Expand)AuthorAge
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Now "Include Self <expr>" handles partially applied functors, cf for example ...Gravatar soubiran2009-11-18
* Allow interactive proofs in module typesGravatar letouzey2009-11-18
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
* Add support for Local Declare ML ModuleGravatar glondu2009-09-29
* Add the option to automatically introduce variables declared before theGravatar msozeau2009-09-22
* Replace call to where_in_path by find_file_in_path in "Locate File"Gravatar glondu2009-09-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 11:19:27 +0000