| Commit message (Expand) | Author | Age |
* | 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-08-01 |
* | 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-17 |
* | Added a Register Inline command for the native compiler. Will be ported to th... | mdenes | 2013-07-10 |
* | Removing SortArgType. | ppedrot | 2013-07-05 |
* | Expurgating the useless difference between List0 and List1 at the | ppedrot | 2013-07-05 |
* | Removing the use of leveled tactics wit_tacticn. It is now handled | ppedrot | 2013-07-02 |
* | Getting rid of IntroPatternArgType. | ppedrot | 2013-06-27 |
* | Removing useless tactic arguments, and using generic arguments | ppedrot | 2013-06-27 |
* | Splitted up Genarg in four different levels: | ppedrot | 2013-06-21 |
* | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot | 2013-06-21 |
* | Adding genarg printer to debugger. | ppedrot | 2013-06-19 |
* | Proof-of-concept: moved four easy-to-handle generic arguments to | ppedrot | 2013-06-18 |
* | Added Genarg as generic argument type. | ppedrot | 2013-06-12 |
* | Uniformizing generic argument types. | ppedrot | 2013-06-06 |
* | Removing useless uses of Gmap. | ppedrot | 2013-05-14 |
* | Use the Hook module here and there. | ppedrot | 2013-05-12 |
* | Now printing body of abbreviations (i.e. notation with a name) with | herbelin | 2013-05-05 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | 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-17 |
* | More functional implementation of locality_flag and program_mode | gareuselesinge | 2013-04-15 |
* | Revised infrastructure for lazy loading of opaque proofs | letouzey | 2013-04-02 |
* | Minor code cleaning in CArray / CList. | ppedrot | 2013-03-23 |
* | 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-21 |
* | Ppvernac: no globalization for printing ltac definitions | letouzey | 2013-03-17 |
* | Pptactic.pr_raw_tactic is now without env argument | letouzey | 2013-03-14 |
* | 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-13 |
* | 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-11 |
* | Use with_state_protection in pr_module_vardecls | gareuselesinge | 2013-03-08 |
* | More monomorphization. | ppedrot | 2013-03-05 |
* | kernel/declarations becomes a pure mli | letouzey | 2013-02-26 |
* | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey | 2013-02-26 |
* | Dir_path --> DirPath | letouzey | 2013-02-19 |
* | 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-18 |
* | Added propagation of evars unification failure reasons for better | herbelin | 2013-02-17 |
* | Useless use of hooks in VernacDefinition. In addition, this was | ppedrot | 2013-02-10 |
* | No reason a priori for using unfiltered env for printing | herbelin | 2013-01-29 |