aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR #6543: Update headers and creditsGravatar Maxime Dénès2018-02-24
|\
* \ Merge PR #6784: New IR in VM: ClambdaGravatar Maxime Dénès2018-02-24
|\ \
* \ \ Merge PR #6819: Document Arguments extra scopes flagGravatar Maxime Dénès2018-02-24
|\ \ \
* \ \ \ Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\ \ \ \
* \ \ \ \ Merge PR #6803: coqdev.el: add space at the end of compile-commandGravatar Maxime Dénès2018-02-24
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6745: [ast] Improve precision of Ast location recognition in serial...Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \
| | | | | | * | New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | * | Fix map iterator on nativelambda.Gravatar Maxime Dénès2018-02-23
| | | | | * | | Document Arguments extra scopes flagGravatar Jasper Hugunin2018-02-22
| |_|_|_|/ / / |/| | | | | |
| * | | | | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
|/ / / / / /
* | | | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predGravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6283: A pre-commit hook to magically fix whitespace issues.Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6740: Adding a sanity check on inductive variance subtyping.Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | |
| | | | | | | | | | | * Update CREDITS.Gravatar Théo Zimmermann2018-02-21
| | | | | | | | | | | * More accurate and complete headers.Gravatar Théo Zimmermann2018-02-21
| | | | | | | | | | | * Mention the CREDITS file in CONTRIBUTING.Gravatar Théo Zimmermann2018-02-21
| | | | | | | | | | | * Remove redundant COPYRIGHT file.Gravatar Théo Zimmermann2018-02-21
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | |
| | | | | | | | | * | coqdev.el: add space at the end of compile-commandGravatar Gaëtan Gilbert2018-02-21
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
| | | | | | | | * | Add CHANGES entry for decimals in preludeGravatar Jason Gross2018-02-20
| | | | | | | | * | Update SearchPattern.out for numeral notationsGravatar Jason Gross2018-02-20
| | | | | | | | * | Doc: add Decimal-related files to index-list.html.templateGravatar Jason Gross2018-02-20
| | | | | | | | * | Decimal goodies : conversion to/from Coq stringsGravatar Pierre Letouzey2018-02-20
| | | | | | | | * | Decimal: proofs that conversions from/to nat,N,Z are bijectionsGravatar Pierre Letouzey2018-02-20
| | | | | | | | * | Decimal: simple representation of base-10 numbersGravatar Pierre Letouzey2018-02-20
| |_|_|_|_|_|_|/ / |/| | | | | | | |
| | | | | | | | * Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Hugo Herbelin2018-02-20
| |_|_|_|_|_|_|/ |/| | | | | | |
| | | | * | | | Adding a test for wish #5532.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Documenting use of primitive entry names for restricting syntax in notations.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Extended documentation for notations referring to binders.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | More structured printing in unicode notations for binders.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Being more flexible on format Adding a warning to be more informativeGravatar Hugo Herbelin2018-02-20
| | | | * | | | User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Gravatar Hugo Herbelin2018-02-20
| | | | * | | | When printing a notation with "match", more flexibility in matching equations.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Using an "as" clause when needed for printing irrefutable patterns.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Refining the strategy for glueing let-ins to a sequence of binders.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | A (significant) simplification in printing notations with recursive binders.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
| | | | * | | | A first step at refreshing and documenting the new feature.Gravatar Hugo Herbelin2018-02-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 16:03:47 +0000