| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-06-01 | Getting rid of Pp.msgnl and Pp.message. | ppedrot |
| 2012-05-30 | Restore compatibility with camlp4 (some missing open Tok) | letouzey |
| 2012-05-29 | remove many excessive open Util & Errors in mli's | letouzey |
| 2012-05-29 | place all pretty-printing files in new dir printing/ | letouzey |
| 2012-05-29 | Extend become a mli-only file in intf/ | letouzey |
| 2012-05-29 | Avoid Dumpglob dependency on Lexer | letouzey |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | Split Egrammar into Egramml and Egramcoq | letouzey |
| 2012-05-29 | No more Univ in grammar.cma | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Strongly reduce the dependencies of grammar.cma, modulo two hacks | letouzey |
| 2012-05-29 | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey |
| 2012-05-29 | Stuff about notation_constr (ex-aconstr) now in notation_ops.ml | letouzey |
