| Age | Commit message (Expand) | Author |
|---|
| 2012-05-29 | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey |
| 2012-04-26 | Program: avoid staying in program mode after a failed Program command | letouzey |
| 2012-04-12 | lib directory is cut in 2 cma. | pboutill |
| 2012-03-30 | Added a command "Unfocused" which returns an error when the proof is | aspiwack |
| 2012-03-30 | Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl | letouzey |
| 2012-03-26 | Slight change in the semantics of arguments scopes: scopes can no | herbelin |
| 2012-03-23 | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey |
| 2012-03-23 | Remove undocumented command "Delete foo" | letouzey |
| 2012-03-23 | Remove old proof-managment commands Suspend/Resume | letouzey |
| 2012-03-14 | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau |
| 2012-03-14 | Integrated obligations/eterm and program well-founded fixpoint building to to... | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-02-14 | Arguments supports extra notation scopes | gareuselesinge |
| 2012-01-23 | Removed a seemingly unused argument in Require of modules, introduced 10 year... | ppedrot |
| 2011-12-21 | sequel of previous commit | letouzey |
| 2011-12-17 | A pass on warning printings. Made systematic the use of msg_warning so | herbelin |
| 2011-12-16 | Moving bullets (-, +, *) into stand-alone commands instead of being | courtieu |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-12-06 | Minor fixes to Arguments | gareuselesinge |
| 2011-11-21 | New Arguments vernacular | gareuselesinge |
| 2011-11-18 | Adding the type infrastructure to handle properly API management of options | ppedrot |
| 2011-11-18 | Restore backward compatibility. ":>" declares subinstances in Class declarati... | msozeau |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-09-12 | Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the... | aspiwack |
| 2011-05-17 | Break circular dependency Proof_global -> Vernacexpr -> Proof_global. | aspiwack |
| 2011-05-13 | New option [Set Bullet Behavior] allows to select the behaviour of bullets. | aspiwack |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-04-06 | Add 'Existing Instances' declaration to declare multiple instances at once. | letouzey |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2011-02-11 | Annotations at functor applications: | letouzey |
| 2011-01-31 | A fine-grain control of inlining at functor application via priority levels | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2011-01-11 | Add "Print Sorted Universes" | glondu |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-02 | Fixing a bug introduced in r12304 (move of interpretation of | herbelin |
| 2010-10-06 | Remove Explain* vernacs | glondu |
| 2010-10-06 | Remove VernacGo | glondu |
| 2010-10-03 | Added multiple implicit arguments rules per name. | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-03 | Added command "Locate Ltac qid". | herbelin |
| 2010-05-19 | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey |
| 2010-04-30 | Fail: a way to check that a command is refused without blocking a script | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | 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-03-29 | Several bug-fixes and improvements of coqdoc | herbelin |
