| Age | Commit message (Expand) | Author |
|---|
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Implemented a full-fledged equality on [constr_expr]. By the way, | ppedrot |
| 2012-10-31 | Change [Hints Resolve] to still accept constrs as arguments | msozeau |
| 2012-10-29 | Fixed #2926: | ppedrot |
| 2012-10-26 | Moved Entries module back to kernel | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-23 | Cleared a purely declarative .ml file and moved its interface to intf/ | ppedrot |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-10-06 | remove useless hidden_flag in TacMutual(Co)Fix | letouzey |
| 2012-10-06 | Tacexpr: revised version that doesn't need -rectypes | letouzey |
| 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-08-24 | Correcting a comment in pattern-matching compilation. | aspiwack |
| 2012-08-11 | Added support for option Local (at module level) in Tactic Notation. | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-07 | Avoid Pp.std_ppcmds in Misctypes.sort_info | 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 | A prototype implementation of a Print Namespace command. | 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-05-29 | Extend become a mli-only file in intf/ | 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 | Glob_term: minor formatting | letouzey |
| 2012-05-29 | Pattern as a mli-only file, operations in Patternops | 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 | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-05-29 | Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml | letouzey |
| 2012-05-29 | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey |
