| Commit message (Expand) | Author | Age |
|---|
| * | global_reference migrated from Libnames to new Globnames, less deps in gramma... |  letouzey | 2012-05-29 |
| * | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey | 2012-05-29 |
| * | Migrate the grammar entry about "Ltac" into g_vernac.ml4. | letouzey | 2012-05-29 |
| * | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey | 2012-05-29 |
| * | Glob_term now mli-only, operations now in Glob_ops | letouzey | 2012-05-29 |
| * | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
| * | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey | 2012-05-29 |
| * | Program: avoid staying in program mode after a failed Program command | letouzey | 2012-04-26 |
| * | Slight change in the semantics of arguments scopes: scopes can no |  herbelin | 2012-03-26 |
| * | Remove undocumented command "Delete foo" | letouzey | 2012-03-23 |
| * | Final part of moving Program code inside the main code. Adapted add_definitio... |  msozeau | 2012-03-14 |
| * | Noise for nothing |  pboutill | 2012-03-02 |
| * | Arguments supports extra notation scopes |  gareuselesinge | 2012-02-14 |
| * | Fix camlp4 compilation | pboutill | 2012-01-31 |
| * | Added an pattern / occurence syntax for vm_compute. |  ppedrot | 2012-01-30 |
| * | Removed a seemingly unused argument in Require of modules, introduced 10 year... | ppedrot | 2012-01-23 |
| * | 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 |
letouzey
herbelin
msozeau
pboutill
gareuselesinge
ppedrot
courtieu
aspiwack
glondu