| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-31 | Merge PR #746: Timing on ci via coq_makefile for various projects | Maxime Dénès | |
| 2017-07-31 | [general] Remove spurious dependency of highparsing on toplevel. | Emilio Jesus Gallego Arias | |
| `G_vernac` was depending on `toplevel` just for parsing the compat number information. IMHO this was not the right place, so I have moved the parsing bits to parsing and updated the files. This allows to finally separate the `toplevel` from Coq, which avoids linking it in alternative toplevels. | |||
| 2017-07-31 | better `try with` scope in `discr_positions` | amblaf | |
| 2017-07-31 | Correcting [build_discriminator] to make the test-suite pass | amblaf | |
| 2017-07-31 | Replacing tclENV with the goal environment | amblaf | |
| In functions match_eqdec and check_unused_names | |||
| 2017-07-31 | env, sigma as first arguments of functions | amblaf | |
| 2017-07-31 | Remove references to Global.env in tactics/*.ml | amblaf | |
| Only in ml files that are not related to Coq commands | |||
| 2017-07-29 | Drop paragraph mentioning Addendum as separate doc. | Théo Zimmermann | |
| As suggested by @herbelin. | |||
| 2017-07-29 | closing bug 5315 | Julien Forest | |
| 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 | 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 | Extraction.tex: mention the possible "From Coq Require Extraction" | letouzey | |
| 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-26 | Fix TypeclassDebug.out after conflicting PR merges | Matthieu Sozeau | |
| 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 | 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 | 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |