aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-28Merge PR #6789: Check whitespace errors per-commit.Maxime Dénès
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
2018-02-28Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...Maxime Dénès
2018-02-28Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...Maxime Dénès
2018-02-28Merge PR #6752: Remove from CircleCI builds that are already taken care of by...Maxime Dénès
2018-02-24Merge PR #6543: Update headers and creditsMaxime Dénès
2018-02-24Merge PR #6784: New IR in VM: ClambdaMaxime Dénès
2018-02-24Merge PR #6819: Document Arguments extra scopes flagMaxime Dénès
2018-02-24Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Maxime Dénès
2018-02-24Merge PR #6803: coqdev.el: add space at the end of compile-commandMaxime Dénès
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-24Merge PR #6745: [ast] Improve precision of Ast location recognition in serial...Maxime Dénès
2018-02-23Check whitespace errors per-commit.Gaëtan Gilbert
2018-02-23New IR in VM: Clambda.Maxime Dénès
2018-02-23Fix map iterator on nativelambda.Maxime Dénès
2018-02-23Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Hugo Herbelin
2018-02-22Document Arguments extra scopes flagJasper Hugunin
2018-02-22Tweak developer documentation.Jim Fehrle
2018-02-22Rename 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-21Remove from CircleCI builds that are already taken care of by Travis.Théo Zimmermann
2018-02-21Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Maxime Dénès
2018-02-21Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predMaxime Dénès
2018-02-21Merge PR #6767: [ci] add elpiMaxime Dénès
2018-02-21Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Maxime Dénès
2018-02-21Merge PR #6283: A pre-commit hook to magically fix whitespace issues.Maxime Dénès
2018-02-21Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...Maxime Dénès
2018-02-21Merge PR #6740: Adding a sanity check on inductive variance subtyping.Maxime Dénès
2018-02-21Update CREDITS.Théo Zimmermann
2018-02-21More accurate and complete headers.Théo Zimmermann
2018-02-21Mention the CREDITS file in CONTRIBUTING.Théo Zimmermann
2018-02-21Remove redundant COPYRIGHT file.Théo Zimmermann
2018-02-21coqdev.el: add space at the end of compile-commandGaëtan Gilbert
2018-02-20Add CHANGES entry for decimals in preludeJason Gross
2018-02-20Update SearchPattern.out for numeral notationsJason Gross
2018-02-20Doc: add Decimal-related files to index-list.html.templateJason Gross
2018-02-20Decimal goodies : conversion to/from Coq stringsPierre Letouzey
2018-02-20Decimal: proofs that conversions from/to nat,N,Z are bijectionsPierre Letouzey
2018-02-20Decimal: simple representation of base-10 numbersPierre Letouzey
2018-02-20Fixes bug #6774 (anomaly with ill-typed template polymorphism).Hugo Herbelin
2018-02-20Adding a test for wish #5532.Hugo Herbelin
2018-02-20Documenting use of primitive entry names for restricting syntax in notations.Hugo Herbelin
2018-02-20Extended documentation for notations referring to binders.Hugo Herbelin
2018-02-20Trying a hack to support {'pat|P} without breaking compatibility.Hugo Herbelin
2018-02-20Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Hugo Herbelin
2018-02-20Change default for notations with variables bound to both terms and binders.Hugo Herbelin
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
2018-02-20Notations: A step in cleaning constr_entry_key.Hugo Herbelin
2018-02-20Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Hugo Herbelin
2018-02-20More flexibility in locating or referring to a notation.Hugo Herbelin