coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-19	Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)	Pierre-Marie Pédrot
2021-01-18	Print primitive constants in debuger	Pierre Roux
2021-01-12	Change the case representation of patterns.	Pierre-Marie Pédrot
2021-01-09	Merge PR #13299: Remember universe instances of constants in notations	coqbot-app[bot]
2021-01-04	Remember universe instances of constants in notations	Jasper Hugunin
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
2020-12-11	Removing non relevant argument binding_kind of GLocalDef.	Hugo Herbelin
2020-12-11	Merge PR #13519: Better primitive type support in custom string and numeral n...	coqbot-app[bot]
2020-12-11	Merge PR #13540: Clean support of primitive integers	Pierre-Marie Pédrot
2020-12-09	Using self-documenting argument names in two exceptions of cases.ml.	Hugo Herbelin
2020-12-09	Constrintern.ml: some naming uniformity.	Hugo Herbelin
2020-12-09	Some documentation in constrintern.ml.	Hugo Herbelin
2020-12-09	Fixing some indentations in constrintern.ml.	Hugo Herbelin
2020-12-09	Constrintern: Code factorization in interning of record fields.	Hugo Herbelin
2020-12-09	Constrintern: Grouping together functions about reference locating.	Hugo Herbelin
2020-12-09	Constrintern cleanup: Centralizing calls to find_appl_head.	Hugo Herbelin
2020-12-09	Fixing support for argument scopes and let-ins while interning cases patterns.	Hugo Herbelin
2020-12-09	Move addition of parameters in asymmetric mode to first phase of pat interning.	Hugo Herbelin
2020-12-09	Removing a useless explicit use of subscopes in interpreting arguments of a n...	Hugo Herbelin
2020-12-09	Constrintern: As in terms, accept @C for C abbreviation in cases patterns.	Hugo Herbelin
2020-12-09	Constrintern: shortcut in cases pattern interning.	Hugo Herbelin
2020-12-04	Better primitive type support in custom string and numeral notations.	Fabian Kunze
2020-12-02	Greatly simplify the conversion functions between Z.t and Uint63.t.	Guillaume Melquiond
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-24	Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a ...	coqbot-app[bot]
2020-11-23	Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...	coqbot-app[bot]
2020-11-23	Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...	coqbot-app[bot]
2020-11-22	Renaming "ident" into "name" in grammar entries, to prevent confusions.	Hugo Herbelin
2020-11-21	Fixes #13432: regression with notations involving coercions caused by #11172.	Hugo Herbelin
2020-11-20	Enforcing when a binding variable has no explicit type in constr_notation.	Hugo Herbelin
2020-11-20	A step towards supporting pattern cast deeplier.	Hugo Herbelin
2020-11-20	Add preliminary support for notations with large class (non-recursive) binders.	Hugo Herbelin
2020-11-20	Rewriting convoluted code of set_var_scope in constrintern.ml.	Hugo Herbelin
2020-11-20	Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...	coqbot-app[bot]
2020-11-20	Use nat_or_var where negative values don't make sense	Jim Fehrle
2020-11-20	Merge PR #13360: Fix incorrect name refreshing when interning a generalized b...	coqbot-app[bot]
2020-11-19	Merge PR #12984: [printing] Order notations by matching precision first, and ...	coqbot-app[bot]
2020-11-18	In recursive notations, accept partial application over the recursive pattern.	Hugo Herbelin
2020-11-17	Merge PR #13390: Intern application arguments in left-to-right order	coqbot-app[bot]
2020-11-17	A reimport of notations now put the corresponding notations again in front.	Hugo Herbelin
2020-11-17	For printing, ordering notations by precision of the pattern.	Hugo Herbelin
2020-11-17	Merge PR #12653: Syntax for specifying cumulative inductives	coqbot-app[bot]
2020-11-16	Fixing alpha-equality of notation interpretations with recursive patterns.	Hugo Herbelin
2020-11-16	Using labels to document match_notation_constr.	Hugo Herbelin
2020-11-16	Fix #9569 (notations collect the spine binding variables at printing time).	Hugo Herbelin
2020-11-16	Merge PR #12690: Mini-fix of Locate for recursive notations using named varia...	coqbot-app[bot]
2020-11-16	Fix incorrect name refreshing when interning a generalized binder	Gaëtan Gilbert
2020-11-16	Merge PR #12685: Propagating scope information in indirect application to a r...	Pierre-Marie Pédrot
2020-11-16	Syntax for specifying cumulative inductives	Gaëtan Gilbert
2020-11-15	Intern application arguments in left-to-right order	Gaëtan Gilbert