| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2013-01-29 | Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-27 | Avoid failure in debugger when printing Ltac names. | herbelin |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-21 | Yet a new reduction tactic in Coq : cbn | pboutill |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-18 | Modulification of mod_bound_id | ppedrot |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
