| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | | | | | Merge PR #6784: New IR in VM: Clambda |  Maxime Dénès | 2018-02-24 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6819: Document Arguments extra scopes flag | Maxime Dénès | 2018-02-24 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism). | Maxime Dénès | 2018-02-24 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6803: coqdev.el: add space at the end of compile-command | Maxime Dénès | 2018-02-24 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6599: Decimals in prelude | Maxime Dénès | 2018-02-24 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6745: [ast] Improve precision of Ast location recognition in serial... | Maxime Dénès | 2018-02-24 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | * | | | | | Check whitespace errors per-commit. |  Gaëtan Gilbert | 2018-02-23 | |
| | | | | | | * | | | | | | | | | | | New IR in VM: Clambda. | Maxime Dénès | 2018-02-23 | |
| | | | | | | * | | | | | | | | | | | Fix map iterator on nativelambda. | Maxime Dénès | 2018-02-23 | |
| | | | | | | | |_|_|_|_|/ / / / / | | | | | | |/| | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion). |  Hugo Herbelin | 2018-02-23 | |
| | |_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | | | | Document Arguments extra scopes flag |  Jasper Hugunin | 2018-02-22 | |
| | |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | Tweak developer documentation. |  Jim Fehrle | 2018-02-22 | |
| | | | | | | | | * | | | | | | Rename release_lexer_state to the more descriptive get_lexer_state. | Jim Fehrle | 2018-02-22 | |
| | | | | | | |_|/ / / / / / | | | | | |/| | | | | | | | ||||
| | * | | | / | | | | | | | | [ast] Improve precision of Ast location recognition in serialization. |  Emilio Jesus Gallego Arias | 2018-02-22 | |
| |/ / / / / / / / / / / / | ||||
| | | | | | | * / / / / / | Remove from CircleCI builds that are already taken care of by Travis. |  Théo Zimmermann | 2018-02-21 | |
| | |_|_|_|_|/ / / / / / |/| | | | | | | | | | | ||||
| * | | | | | | | | | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred` | Maxime Dénès | 2018-02-21 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred | Maxime Dénès | 2018-02-21 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6767: [ci] add elpi | Maxime Dénès | 2018-02-21 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585) | Maxime Dénès | 2018-02-21 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6283: A pre-commit hook to magically fix whitespace issues. | Maxime Dénès | 2018-02-21 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the... | Maxime Dénès | 2018-02-21 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6740: Adding a sanity check on inductive variance subtyping. | Maxime Dénès | 2018-02-21 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | | | | | Update CREDITS. | Théo Zimmermann | 2018-02-21 | |
| | | | | | | | | | | | * | | | | | | More accurate and complete headers. | Théo Zimmermann | 2018-02-21 | |
| | | | | | | | | | | | * | | | | | | Mention the CREDITS file in CONTRIBUTING. | Théo Zimmermann | 2018-02-21 | |
| | | | | | | | | | | | * | | | | | | Remove redundant COPYRIGHT file. | Théo Zimmermann | 2018-02-21 | |
| | |_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | coqdev.el: add space at the end of compile-command | Gaëtan Gilbert | 2018-02-21 | |
| | |_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | Add CHANGES entry for decimals in prelude |  Jason Gross | 2018-02-20 | |
| | | | | | | | | * | | | | | | | Update SearchPattern.out for numeral notations | Jason Gross | 2018-02-20 | |
| | | | | | | | | * | | | | | | | Doc: add Decimal-related files to index-list.html.template | Jason Gross | 2018-02-20 | |
| | | | | | | | | * | | | | | | | Decimal goodies : conversion to/from Coq strings |  Pierre Letouzey | 2018-02-20 | |
| | | | | | | | | * | | | | | | | Decimal: proofs that conversions from/to nat,N,Z are bijections | Pierre Letouzey | 2018-02-20 | |
| | | | | | | | | * | | | | | | | Decimal: simple representation of base-10 numbers | Pierre Letouzey | 2018-02-20 | |
| | |_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | Fixes bug #6774 (anomaly with ill-typed template polymorphism). | Hugo Herbelin | 2018-02-20 | |
| | |_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | overlay for ltac2 and Equations |  Enrico Tassi | 2018-02-20 | |
| | | | | | | | | | | | | * | proofview: goals come with a state | Enrico Tassi | 2018-02-20 | |
| | |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | ||||
| | | | | | | | | | * | | | Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v). | Hugo Herbelin | 2018-02-20 | |
| | |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | ||||
| | | | | * | | | | | | | Adding a test for wish #5532. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Documenting use of primitive entry names for restricting syntax in notations. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Extended documentation for notations referring to binders. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Trying a hack to support {'pat|P} without breaking compatibility. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Change default for notations with variables bound to both terms and binders. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Notations: Adding modifiers to tell which kind of binder a constr can parse. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Notations: A step in cleaning constr_entry_key. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | More flexibility in locating or referring to a notation. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | More structured printing in unicode notations for binders. | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | Being more flexible on format Adding a warning to be more informative | Hugo Herbelin | 2018-02-20 | |
| | | | | * | | | | | | | User-level support for Gonthier-Ssreflect's "if t then pat then u else v". | Hugo Herbelin | 2018-02-20 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |