| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-28 | Parameterizing FFI functions for parameterized types. | Pierre-Marie Pédrot | |
| 2017-07-28 | Moving the Ltac2 FFI to a separate file. | Pierre-Marie Pédrot | |
| 2017-07-28 | Merge PR #923: [api] Fix base_include LTAC parts. | Maxime Dénès | |
| 2017-07-28 | Merge PR #889: Removing template polymorphism for definitions. | Maxime Dénès | |
| 2017-07-28 | Merge PR #888: Stronger kernel types | Maxime Dénès | |
| 2017-07-28 | Merge PR #823: Async off in Windows by default in CoqIDE | Maxime Dénès | |
| 2017-07-28 | Merge PR #782: Update API for fiat | Maxime Dénès | |
| 2017-07-28 | Allowing generic patterns in let-bindings. | Pierre-Marie Pédrot | |
| 2017-07-28 | Fix some coq-tex errors in the reference manual. | Guillaume Melquiond | |
| 2017-07-28 | Fix documentation of Hint Mode (bug #4911). | Guillaume Melquiond | |
| 2017-07-28 | Fix shuffled documentation. | Guillaume Melquiond | |
| 2017-07-28 | Merge PR #852: Makefile: fails if some .vo or .cm* file has no source | Maxime Dénès | |
| 2017-07-27 | Add missing paragraph to introduction | Benjamin Pierce | |
| 2017-07-27 | Fixing bug #5671 (specialize unclean wrt Metas). | Hugo Herbelin | |
| 2017-07-27 | Factorizing code for constructors and tuples. | Pierre-Marie Pédrot | |
| 2017-07-27 | Extraction.tex: mention the possible "From Coq Require Extraction" | letouzey | |
| 2017-07-27 | Cleaning up code in internalization. | Pierre-Marie Pédrot | |
| 2017-07-27 | Using thunks in the horrible Ltac2 example. | Pierre-Marie Pédrot | |
| 2017-07-27 | Fix expansion of toplevel let-rec after the constructor / constant split. | Pierre-Marie Pédrot | |
| 2017-07-27 | Extraction TestCompile documented + mentionned in CHANGES | Pierre Letouzey | |
| Also includes a minor fix of the Extraction doc (a Require was missing). | |||
| 2017-07-27 | test-suite: more use of the new command Extraction TestCompile | Pierre Letouzey | |
| 2017-07-27 | [toplevel] Remove long ago deprecated and NOOP options. | Emilio Jesus Gallego Arias | |
| Minor clean up, no sense in having these as they do nothing. | |||
| 2017-07-27 | [make] remove compat5 file. | Emilio Jesus Gallego Arias | |
| It is empty and not used anymore. | |||
| 2017-07-27 | [api] Fix base_include LTAC parts. | Emilio Jesus Gallego Arias | |
| 2017-07-27 | Fixing one part of #5669 (unification heuristics sensitive to choice of names). | Hugo Herbelin | |
| This surprising bug was caused by an Id.Set which was ordering solutions to variable-projection problems in ascii order. We fix it by re-considering the variables involved in the solutions using the declaration order. Note that in practice, this implies preferring a dependent solution over a non-dependent one. | |||
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-27 | Adding necessary primitives to do pattern-matching over constr. | Pierre-Marie Pédrot | |
| 2017-07-26 | Fix TypeclassDebug.out after conflicting PR merges | Matthieu Sozeau | |
| 2017-07-26 | Adding an example file | Pierre-Marie Pédrot | |
| 2017-07-26 | Tentative fix of parsing of product types. | Pierre-Marie Pédrot | |
| 2017-07-26 | Dedicated module for ident type. | Pierre-Marie Pédrot | |
| 2017-07-26 | test-suite/success/extraction.v : add some Extraction TestCompile | Pierre Letouzey | |
| 2017-07-26 | Enrich test file 4720.v with a compilation test of the extracted code | Pierre Letouzey | |
| 2017-07-26 | adding a test-suite file 4709.v (thanks to the new command Extraction ↵ | Pierre Letouzey | |
| TestCompile) | |||
| 2017-07-26 | Extraction: reduce primitive projections in types (fix bug 4709) | Pierre Letouzey | |
| 2017-07-26 | Do not expand trivial patterns in functions. | Pierre-Marie Pédrot | |
| 2017-07-26 | Ensuring that inductive constructors are always capitalized. | Pierre-Marie Pédrot | |
| 2017-07-26 | Adding a file for testing typing. | Pierre-Marie Pédrot | |
| 2017-07-26 | kernel: bugfix in filter_stack_domain. | Matthieu Sozeau | |
| It did not consider that the argument might be higher-order, e.g. [nat -> I]. | |||
| 2017-07-26 | Fix typo in error message | Pierre-Marie Pédrot | |
| 2017-07-26 | Better typing errors for function types. | Pierre-Marie Pédrot | |
| 2017-07-26 | Lightweight quotation syntax for terms and idents. | Pierre-Marie Pédrot | |
| 2017-07-26 | Remove a few useless evar-normalizations in printing code. | Pierre-Marie Pédrot | |
| 2017-07-26 | Add a comment regarding the specialization of the combinator in Detyping. | Pierre-Marie Pédrot | |
| 2017-07-26 | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs ↵ | Maxime Dénès | |
| 4844 and 4824) | |||
| 2017-07-26 | Merge PR #910: Add [opam update] and online repository to gitlab CI script. | Maxime Dénès | |
| 2017-07-26 | Removing default evar-normalization for ARGUMENT EXTEND. | Pierre-Marie Pédrot | |
| This fixes bug 5650: evar (x : Prop) should not be slow. | |||
| 2017-07-26 | Merge PR #886: Fixing what was presumably a typo in the naming conventions file | Maxime Dénès | |
| 2017-07-26 | Merge PR #902: Only perform profile initialization and printing when the ↵ | Maxime Dénès | |
| flag is set. | |||
| 2017-07-26 | Removing template polymorphism for definitions. | Pierre-Marie Pédrot | |
| The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |