| Commit message (Expand) | Author | Age |
* | Reverted previous commit, which broke library compilation. | ppedrot | 2012-01-20 |
* | This is a quick hack to permit the parsing of the locality flag in the Progra... | ppedrot | 2012-01-20 |
* | Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}. | msozeau | 2012-01-19 |
* | A pass on warning printings. Made systematic the use of msg_warning so | herbelin | 2011-12-17 |
* | Fixing previous commit which was bugging on tactics preceded by goal number (... | courtieu | 2011-12-16 |
* | Moving bullets (-, +, *) into stand-alone commands instead of being | courtieu | 2011-12-16 |
* | Minor fixes to Arguments | gareuselesinge | 2011-12-06 |
* | Continuing r14747 being actually incomplete (flushing warnings and | herbelin | 2011-11-30 |
* | Preventing Implicit Arguments warning to be shown in non verbose mode | herbelin | 2011-11-30 |
* | New Arguments vernacular | gareuselesinge | 2011-11-21 |
* | Adding the type infrastructure to handle properly API management of options | ppedrot | 2011-11-18 |
* | Fix parsing of :>> and backtrack correctly on the cache of hints for local co... | msozeau | 2011-11-18 |
* | Restore backward compatibility. ":>" declares subinstances in Class declarati... | msozeau | 2011-11-18 |
* | Merge subinstances branch by me and Tom Prince. | msozeau | 2011-11-17 |
* | Quick improvement of some error messages related to module application | herbelin | 2011-08-30 |
* | Adding a new syntax for BeginSubproof and EndSubproof, namely { and }. | courtieu | 2011-07-05 |
* | Break circular dependency Proof_global -> Vernacexpr -> Proof_global. | aspiwack | 2011-05-17 |
* | New option [Set Bullet Behavior] allows to select the behaviour of bullets. | aspiwack | 2011-05-13 |
* | G_vernac can be parsed without grammar.cma | letouzey | 2011-04-26 |
* | Revert "Add [Polymorphic] flag for defs" | msozeau | 2011-04-13 |
* | Add [Polymorphic] flag for defs | msozeau | 2011-04-13 |
* | Add 'Existing Instances' declaration to declare multiple instances at once. | letouzey | 2011-04-06 |
* | - Remove useless grammar rule | msozeau | 2011-03-23 |
* | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
* | - Fix treatment of globality flag for typeclass instance hints (they | msozeau | 2011-02-14 |
* | Annotations at functor applications: | letouzey | 2011-02-11 |
* | A fine-grain control of inlining at functor application via priority levels | letouzey | 2011-01-31 |
* | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey | 2011-01-28 |
* | Add "Print Sorted Universes" | glondu | 2011-01-11 |
* | Remove obsolete script univdot, update dev doc about universes | glondu | 2010-12-24 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | Don't interpret VMcast as an ordinary type cast in Definition a := t <: T. | herbelin | 2010-12-09 |
* | SearchAbout: who has never been annoyed by the [ ] syntax ? | letouzey | 2010-11-19 |
* | Export the "bullet" grammar entry | glondu | 2010-10-08 |
* | Added multiple implicit arguments rules per name. | herbelin | 2010-10-03 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Extension of the recursive notations mechanism | herbelin | 2010-07-22 |
* | Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt). | herbelin | 2010-07-22 |
* | Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword). | herbelin | 2010-07-18 |
* | Using vernac parsing for Function | jforest | 2010-06-08 |
* | A new command Compute foo, shortcut for Eval vm_compute in foo | letouzey | 2010-06-04 |
* | Added command "Locate Ltac qid". | herbelin | 2010-06-03 |
* | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
* | Nicer representation of tokens, more independant of camlp* | letouzey | 2010-05-19 |
* | static (and shared) camlp4use instead of per-file declaration | letouzey | 2010-05-19 |
* | Fail: a way to check that a command is refused without blocking a script | letouzey | 2010-04-30 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
* | Applying François Garillot's patch (#2261 in bug tracker) for extended | herbelin | 2010-04-22 |
* | Several bug-fixes and improvements of coqdoc | herbelin | 2010-03-29 |