coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-01-13	Make sure "Print Module" write a dot at the end of inductive definitions.	Guillaume Melquiond

2018-10-10	Miscellaneous refinements/cleaning of module printing.	Hugo Herbelin
	This refines the fix to #2169 by distinguishing the short and non-short printing modes. This prepares functionalization of printers by always passing env rather than setting env to None in short mode. This is not strictly necessary for the env which is not used for printing global references but it shall be more consistent in style when passing e.g. the nametab functionally. We however keep the fallback printer used in case of error while printing: due to missing registration of submodule fields in the nametab, printing with types does not work if there are references to an inner module.
2016-10-01	Fix bug #4661: Cannot mask the absolute name.	Pierre-Marie Pédrot
	The patch is quite dumb: it essentially consists in alpha-renaming bound module names when printing a functor, by checking that the name was not already present, and generating a fresh one otherwise.
2015-07-27	Output test for bug #2169.	Pierre-Marie Pédrot