| Age | Commit message (Expand) | Author |
|---|
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-22 | Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located. | herbelin |
| 2012-12-21 | Yet a new reduction tactic in Coq : cbn | pboutill |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-04 | Early translation of camlp4/camlp5 located errors into coq-located | herbelin |
| 2012-11-25 | Monomorphization (parsing) | ppedrot |
| 2012-11-15 | backtrack too much commited files in the last commit. | courtieu |
| 2012-11-15 | Fixing emacs diff bug with .dir-locals.el. | courtieu |
| 2012-11-13 | More monomorphizations | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-11-07 | Fix reference_or_constr grammar rule to accept @t as a constr | gareuselesinge |
| 2012-10-31 | Change [Hints Resolve] to still accept constrs as arguments | msozeau |
| 2012-10-29 | Fixed #2926: | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-10-15 | Egramml: minor simplification | letouzey |
| 2012-10-06 | restore compatibility with camlp5 < 6.00 | letouzey |
| 2012-10-06 | still some more dead code removal | letouzey |
| 2012-10-06 | remove useless hidden_flag in TacMutual(Co)Fix | letouzey |
| 2012-10-05 | Fix a confusion between types of locations in an untyped part of the parser | letouzey |
| 2012-10-04 | Adding a nominal typing layer to Metasyntax in order to clarify | ppedrot |
| 2012-10-04 | Moved Compat to parsing. This permits to break the dependency of the | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-10-02 | avoid referring to Term in constrexpr.mli and glob_term.mli | letouzey |
| 2012-10-01 | Added a new tactical infoH tac, that displays the names of hypothesis created... | courtieu |
| 2012-09-18 | More cleanup of Util: utf8 aspects moved to a new file unicode.ml | letouzey |
| 2012-09-17 | More cleaning on Utils and CList. Some parts of the code being | ppedrot |
| 2012-09-14 | Partial revert of Yann commit in order to use CLib.List when opening | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-11 | Added support for option Local (at module level) in Tactic Notation. | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-02 | Bigint: new functions of_int and to_int, 2nd arg of pow in int | letouzey |
| 2012-07-19 | Getting rid of the undocumented [complete] tactic, which was | ppedrot |
| 2012-07-11 | Re-allow Reset in compiled files | letouzey |
| 2012-07-09 | destruct: full compatibility with former _eqn syntax | letouzey |
| 2012-07-09 | The tactic remember now accepts a final eqn:H option (grant wish #2489) | letouzey |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-07-06 | Two adaptations after the changes of level of -> | letouzey |
| 2012-07-06 | A prototype implementation of a Print Namespace command. | aspiwack |
| 2012-07-06 | Fixes a bug in the parsing of the grammar entry dirpath which would, | aspiwack |
| 2012-07-05 | Notation: a new annotation "compat 8.x" extending "only parsing" | letouzey |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-14 | Internalization of pattern is done in two phases. | pboutill |
| 2012-06-04 | Fixing previous commit (something strange happened...) | ppedrot |
| 2012-06-04 | Replacing some str with strbrk | ppedrot |
| 2012-06-04 | Added a color output to Coqtop. | ppedrot |
