coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-15	Propagating scope information in indirect application to a reference.	Hugo Herbelin
2020-02-25	Fixing residual bug of #11120.	Hugo Herbelin
2020-02-22	Inherit scopes and implicit sign. in notations for partially applied pattern.	Hugo Herbelin
2020-02-22	Inherit argument scopes in notations to expressions of the form @f.	Hugo Herbelin
2020-02-22	Propagate implicit arguments in all notations for partial applications.	Hugo Herbelin
2020-02-22	Fixing a bug introduced in PR #10832 (new format specific to a given notation).	Hugo Herbelin
2019-12-10	Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).	Hugo Herbelin
2019-05-10	Use Print Custom Grammar to inspect custom entries	Jasper Hugunin
2019-02-19	Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.	Hugo Herbelin
2018-07-29	Supporting locality flag for custom entries + compatibility with modules.	Hugo Herbelin
2018-07-29	A test on the different ways to indicate the levels of a rule.	Hugo Herbelin
2018-02-20	Notations: Adding modifiers to tell which kind of binder a constr can parse.	Hugo Herbelin
2018-02-20	Notations: Do not consider a non-occurring variable as a binder-only variable.	Hugo Herbelin
2017-11-20	Fixing factorization of recursive notations in the case of an atomic separator.	Hugo Herbelin
2017-11-14	One more step in fixing #5762 ("where" clause).	Hugo Herbelin
2016-03-13	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin
2016-03-13	Adding a file summarizing the inconsistencies in interpreting implicit	Hugo Herbelin