aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-07-28Parameterizing FFI functions for parameterized types.Pierre-Marie Pédrot
2017-07-28Moving the Ltac2 FFI to a separate file.Pierre-Marie Pédrot
2017-07-28Merge PR #923: [api] Fix base_include LTAC parts.Maxime Dénès
2017-07-28Merge PR #889: Removing template polymorphism for definitions.Maxime Dénès
2017-07-28Merge PR #888: Stronger kernel typesMaxime Dénès
2017-07-28Merge PR #823: Async off in Windows by default in CoqIDEMaxime Dénès
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-28Allowing generic patterns in let-bindings.Pierre-Marie Pédrot
2017-07-28Fix some coq-tex errors in the reference manual.Guillaume Melquiond
2017-07-28Fix documentation of Hint Mode (bug #4911).Guillaume Melquiond
2017-07-28Fix shuffled documentation.Guillaume Melquiond
2017-07-28Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceMaxime Dénès
2017-07-27Add missing paragraph to introductionBenjamin Pierce
2017-07-27Fixing bug #5671 (specialize unclean wrt Metas).Hugo Herbelin
2017-07-27Factorizing code for constructors and tuples.Pierre-Marie Pédrot
2017-07-27Extraction.tex: mention the possible "From Coq Require Extraction"letouzey
2017-07-27Cleaning up code in internalization.Pierre-Marie Pédrot
2017-07-27Using thunks in the horrible Ltac2 example.Pierre-Marie Pédrot
2017-07-27Fix expansion of toplevel let-rec after the constructor / constant split.Pierre-Marie Pédrot
2017-07-27Extraction TestCompile documented + mentionned in CHANGESPierre Letouzey
2017-07-27test-suite: more use of the new command Extraction TestCompilePierre Letouzey
2017-07-27[toplevel] Remove long ago deprecated and NOOP options.Emilio Jesus Gallego Arias
2017-07-27[make] remove compat5 file.Emilio Jesus Gallego Arias
2017-07-27[api] Fix base_include LTAC parts.Emilio Jesus Gallego Arias
2017-07-27Fixing one part of #5669 (unification heuristics sensitive to choice of names).Hugo Herbelin
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-27Adding necessary primitives to do pattern-matching over constr.Pierre-Marie Pédrot
2017-07-26Fix TypeclassDebug.out after conflicting PR mergesMatthieu Sozeau
2017-07-26Adding an example filePierre-Marie Pédrot
2017-07-26Tentative fix of parsing of product types.Pierre-Marie Pédrot
2017-07-26Dedicated module for ident type.Pierre-Marie Pédrot
2017-07-26test-suite/success/extraction.v : add some Extraction TestCompilePierre Letouzey
2017-07-26Enrich test file 4720.v with a compilation test of the extracted codePierre Letouzey
2017-07-26adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...Pierre Letouzey
2017-07-26Extraction: reduce primitive projections in types (fix bug 4709)Pierre Letouzey
2017-07-26Do not expand trivial patterns in functions.Pierre-Marie Pédrot
2017-07-26Ensuring that inductive constructors are always capitalized.Pierre-Marie Pédrot
2017-07-26Adding a file for testing typing.Pierre-Marie Pédrot
2017-07-26kernel: bugfix in filter_stack_domain.Matthieu Sozeau
2017-07-26Fix typo in error messagePierre-Marie Pédrot
2017-07-26Better typing errors for function types.Pierre-Marie Pédrot
2017-07-26Lightweight quotation syntax for terms and idents.Pierre-Marie Pédrot
2017-07-26Remove a few useless evar-normalizations in printing code.Pierre-Marie Pédrot
2017-07-26Add a comment regarding the specialization of the combinator in Detyping.Pierre-Marie Pédrot
2017-07-26Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Maxime Dénès
2017-07-26Merge PR #910: Add [opam update] and online repository to gitlab CI script.Maxime Dénès
2017-07-26Removing default evar-normalization for ARGUMENT EXTEND.Pierre-Marie Pédrot
2017-07-26Merge PR #886: Fixing what was presumably a typo in the naming conventions fileMaxime Dénès
2017-07-26Merge PR #902: Only perform profile initialization and printing when the flag...Maxime Dénès
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 03:11:53 +0000