| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2017-07-26 | Merge PR #894: Fixing a little location bug with recursive binders | Maxime Dénès | |
| 2017-07-26 | Merge PR #882: Adding a V8.7 compatibility version number. | Maxime Dénès | |
| 2017-07-26 | Avoiding a variable shadowing in the kernel. | Pierre-Marie Pédrot | |
| This ought to ease the understanding of the code. | |||
| 2017-07-26 | Statically ensuring that inlined entries out of the kernel have no effects. | Pierre-Marie Pédrot | |
| This was an easy to prove property that I somehow overlooked. | |||
| 2017-07-26 | Further simplication: do not recreate entries for side-effects. | Pierre-Marie Pédrot | |
| This is actually useless, the code does not depend on the value of the entry for side-effects. | |||
| 2017-07-26 | Remove a horrendous hack in Declare to retrieve exported side-effects. | Pierre-Marie Pédrot | |
| Instead of relying on a mutable state in the object pushed on the libstack, we export an API in the kernel that exports the side-effects of a given entry in the global environment. | |||
| 2017-07-26 | More precise type of entries capturing their lack of side-effects. | Pierre-Marie Pédrot | |
| We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants. | |||
| 2017-07-26 | Using a record type for Cooking.result. | Pierre-Marie Pédrot | |
| 2017-07-26 | More precise type for universe entries. | Pierre-Marie Pédrot | |
| We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure. | |||
| 2017-07-26 | Merge PR #885: Removing a dummy parameter in some FMapPositive statements. | Maxime Dénès | |
| 2017-07-26 | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin | |
| Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing. | |||
| 2017-07-26 | Merge PR #868: Fix debug trace of typeclasses eauto. | Maxime Dénès | |
| 2017-07-26 | Merge PR #845: Add Z.mod_div lemma to standard library. | Maxime Dénès | |
| 2017-07-26 | Merge PR #905: [api] Remove type equalities from API. | Maxime Dénès | |
| 2017-07-26 | Merge PR #857: Extraction: various fixes related with bug 4720 | Maxime Dénès | |
| 2017-07-26 | Merge PR #859: Extraction TestCompile | Maxime Dénès | |
| 2017-07-26 | Merge PR #808: [api] Put some order in API.mli | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |