aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Expand)AuthorAge
...
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 tooGravatar herbelin2010-09-18
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Some fine-tuning after removal of automatic imports of coercions in r13310Gravatar herbelin2010-07-23
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Added command "Locate Ltac qid".Gravatar herbelin2010-06-03
* Fail: a way to check that a command is refused without blocking a scriptGravatar letouzey2010-04-30
* 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
* Applying François Garillot's patch (#2261 in bug tracker) for extendedGravatar herbelin2010-04-22
* Small improvements around coqdoc (including fix for bug #2288)Gravatar herbelin2010-03-30
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* Fix "Existing Instance" to handle globality information and "ExistingGravatar msozeau2009-12-27
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:20:52 +0000