coq - The formal proof system

Age	Commit message (Expand)	Author
2021-04-07	[abbreviation] allow the user to set arguments scope	Enrico Tassi
2021-04-07	cleanup: remove confusing sharing	Enrico Tassi
2021-04-07	cleanup: less exceptions, removal of try_interp_name_alias	Enrico Tassi
2021-03-26	[recordops] complete API rewrite; the module is now called [structures]	Enrico Tassi
2021-01-04	Remember universe instances of constants in notations	Jasper Hugunin
2020-12-11	Removing non relevant argument binding_kind of GLocalDef.	Hugo Herbelin
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-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-22	Renaming "ident" into "name" in grammar entries, to prevent confusions.	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 #13360: Fix incorrect name refreshing when interning a generalized b...	coqbot-app[bot]
2020-11-17	Merge PR #13390: Intern application arguments in left-to-right order	coqbot-app[bot]
2020-11-17	Merge PR #12653: Syntax for specifying cumulative inductives	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
2020-11-15	Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.	Hugo Herbelin
2020-11-15	Propagating scope information in indirect application to a reference.	Hugo Herbelin
2020-11-12	Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...	Pierre-Marie Pédrot
2020-11-06	Merge PR #13255: Fixes #13244: support for coercions in Search	coqbot-app[bot]
2020-11-05	Minor cut elimination in the code of constrintern.ml.	Hugo Herbelin
2020-11-05	Accept local variables in mixed terms and binders of notations.	Hugo Herbelin
2020-11-05	Passing full interning env to pattern interning, for better control.	Hugo Herbelin
2020-11-05	Notations: Giving a consistent role to global references occurring patterns.	Hugo Herbelin
2020-11-04	Typing patterns and using type constraints in Search.	Hugo Herbelin
2020-11-04	Adding a typed interpretation of patterns.	Hugo Herbelin
2020-11-04	Factorizing UState.make* through UState.from_env, to highlight the similarity.	Hugo Herbelin
2020-11-04	Moving interpretation of user-level universes in constrintern.ml.	Hugo Herbelin
2020-10-30	Renaming Numeral into Number	Pierre Roux
2020-10-10	Add location in existential variable names (CEvar/GEvar).	Hugo Herbelin
2020-09-30	interp_context_evars: removed unused [shift] argument	Gaëtan Gilbert
2020-08-15	Document semantic restriction on patterns	Jim Fehrle
2020-07-17	Merge PR #12631: Fix record pattern interpretation with implicit arguments	Emilio Jesus Gallego Arias
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-03	Fix #11121: Simultaneous definition of term and notation in custom grammar	Maxime Dénès