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