| Age | Commit message (Expand) | Author |
| 2013-08-01 | Added a Print Debug GC command that displays the current state of | ppedrot |
| 2013-08-01 | Added printing of instance priority to the Print Instances command. | ppedrot |
| 2013-08-01 | Granting bug #3098: adding priority to Existing Instances. | ppedrot |
| 2013-07-17 | Declaremods: major refactoring, stop duplicating libobjects in modules | letouzey |
| 2013-07-17 | Lib.contents () instead of Lib.contents_after None | letouzey |
| 2013-07-17 | More dynamic argument scopes | letouzey |
| 2013-07-10 | Added a Register Inline command for the native compiler. Will be ported to th... | mdenes |
| 2013-07-05 | Removing SortArgType. | ppedrot |
| 2013-07-05 | Expurgating the useless difference between List0 and List1 at the | ppedrot |
| 2013-07-02 | Removing the use of leveled tactics wit_tacticn. It is now handled | ppedrot |
| 2013-06-27 | Getting rid of IntroPatternArgType. | ppedrot |
| 2013-06-27 | Removing useless tactic arguments, and using generic arguments | ppedrot |
| 2013-06-21 | Splitted up Genarg in four different levels: | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-19 | Adding genarg printer to debugger. | ppedrot |
| 2013-06-18 | Proof-of-concept: moved four easy-to-handle generic arguments to | ppedrot |
| 2013-06-12 | Added Genarg as generic argument type. | ppedrot |
| 2013-06-06 | Uniformizing generic argument types. | ppedrot |
| 2013-05-14 | Removing useless uses of Gmap. | ppedrot |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-05 | Now printing body of abbreviations (i.e. notation with a name) with | herbelin |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-17 | Renaming SearchAbout into Search and Search into SearchHead. | herbelin |
| 2013-04-17 | Improving error message in explain_cannot_find_well_typed_abstraction: | herbelin |
| 2013-04-15 | More functional implementation of locality_flag and program_mode | gareuselesinge |
| 2013-04-02 | Revised infrastructure for lazy loading of opaque proofs | letouzey |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-03-21 | Robust display of NotConvertibleTypeField errors (fix #3008, #2995) | letouzey |
| 2013-03-21 | Printmod: handle more examples thanks to better nametab use | letouzey |
| 2013-03-21 | Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983) | letouzey |
| 2013-03-17 | Ppvernac: no globalization for printing ltac definitions | letouzey |
| 2013-03-14 | Pptactic.pr_raw_tactic is now without env argument | letouzey |
| 2013-03-13 | Modules and ppvernac, sequel of Enrico's commit 16261 | letouzey |
| 2013-03-13 | Declaremods: a few syntactic improvements | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 5) | letouzey |
| 2013-03-11 | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-03-08 | Use with_state_protection in pr_module_vardecls | gareuselesinge |
| 2013-03-05 | More monomorphization. | ppedrot |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-02-26 | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-02-18 | Removing Exc_located and using the new exception enrichement | ppedrot |
| 2013-02-18 | use List.rev_map whenever possible | letouzey |
| 2013-02-18 | Minor code cleanups, especially take advantage of Dir_path.is_empty | letouzey |
| 2013-02-17 | Added propagation of evars unification failure reasons for better | herbelin |
| 2013-02-10 | Useless use of hooks in VernacDefinition. In addition, this was | ppedrot |
| 2013-01-29 | No reason a priori for using unfiltered env for printing | herbelin |