| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-24 | Ensuring that the evar name is preserved by "rename" as it is already | Hugo Herbelin | |
| the case for clear and the conversion tactics. | |||
| 2016-09-24 | Adding a test for bug #5096. | Pierre-Marie Pédrot | |
| 2016-09-23 | Fix bug #5096: [vm_compute] is exponentially slower than [native_compute]. | Pierre-Marie Pédrot | |
| The fix is essentially a revert of f22ad60 that introduced the use of the pretyper version of whd_all instead of the one from the kernel. The exact cause of slowness of the pretyper version is still to be investigated, but it is believed that it is due to a call-by-name strategy, to compare with call-by-need in the kernel. Note that there is still something fishy in presence of evars. Technically vm_compute does not handle them, but if this comes to be the case, it might be worthwile to use an evar-aware variant of whd_all. | |||
| 2016-09-23 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-23 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-22 | coqc -o now places .glob file near .vo file | Enrico Tassi | |
| All compilation (by)products are placed where -o specifies. Used to be the case for .vo, .vio, .aux but not .glob | |||
| 2016-09-22 | typos | Enrico Tassi | |
| 2016-09-22 | Revert "Merge remote-tracking branch 'github/pr/283' into trunk" | Maxime Dénès | |
| I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb. | |||
| 2016-09-22 | Merge remote-tracking branch 'github/pr/283' into trunk | Maxime Dénès | |
| Was PR#283: Stylistic improvements in intf/decl_kinds.mli. | |||
| 2016-09-22 | Fixing #5095 (non relevant too strict test in let-in abstraction). | Hugo Herbelin | |
| 2016-09-21 | Removing dead code in CoqIDE. | Pierre-Marie Pédrot | |
| There was a pile of dead code inherited from Cameleon just sitting around and not used at all. This code was introduced in 2003 and never actually used. | |||
| 2016-09-21 | Fix an error-prone error API. | Pierre-Marie Pédrot | |
| 2016-09-21 | Merging Stdarg and Constrarg. | Pierre-Marie Pédrot | |
| There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore. | |||
| 2016-09-21 | Fix description of change in intro semantics. | Maxime Dénès | |
| 2016-09-20 | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status. | Maxime Dénès | |
| The new name makes it more obvious what is meant here by "kind". We leave Decl_kinds.binding_kind as a deprecated alias for plugin compatibility. We also replace bool with implicit_status in a few places in the codebase. | |||
| 2016-09-20 | Stylistic improvements in intf/decl_kinds.mli. | Maxime Dénès | |
| We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic". | |||
| 2016-09-20 | Remove dead code in library/lib.ml. | Maxime Dénès | |
| 2016-09-19 | Replace { command ; } with ( command ) | Erik Martin-Dorel | |
| as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output. | |||
| 2016-09-19 | Fix typos in RefMan-uti.tex. | Erik Martin-Dorel | |
| - Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace. | |||
| 2016-09-19 | Fixing test FunExt.v. | Hugo Herbelin | |
| 2016-09-19 | Fix warning when using Variables at toplevel. | Maxime Dénès | |
| 2016-09-19 | extensionality: Handle dependently-used hypotheses | Jason Gross | |
| 2016-09-19 | Adding an "extensionality in H" tactic which applies functional | Hugo Herbelin | |
| extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples. | |||
| 2016-09-17 | Fix indentation of -profile-ltac in -help | Jason Gross | |
| 2016-09-17 | Further "decide equality" tests on demand of Jason. | Hugo Herbelin | |
| 2016-09-16 | Doc: [Reset Ltac Profile] is not synchronized | Jason Gross | |
| 2016-09-16 | Addressing OCaml compilation warnings. | Hugo Herbelin | |
| One of them revealed a true bug. | |||
| 2016-09-16 | Adding variants enter_one and refine_one which assume that exactly one | Hugo Herbelin | |
| goal is under focus and which support returning a relevant output. | |||
| 2016-09-16 | Make the Coq codebase independent from Ltac-related code. | Pierre-Marie Pédrot | |
| We untangle many dependencies on Ltac datastructures and modules from the lower strata, resulting in a self-contained ltac/ folder. While not a plugin yet, the change is now very easy to perform. The main API changes have been documented in the dev/doc/changes file. The patches are quite rough, and it may be the case that some parts of the code can migrate back from ltac/ to a core folder. This should be decided on a case-by-case basis, according to a more long-term consideration of what is exactly Ltac-dependent and whatnot. | |||
| 2016-09-15 | Documenting API changes. | Pierre-Marie Pédrot | |
| 2016-09-15 | Moving Tacexpr to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Made Ppanotation Ltac-agnostic. | Pierre-Marie Pédrot | |
| 2016-09-15 | Added a test file for contradiction. | Hugo Herbelin | |
| 2016-09-15 | Untangling Tacexpr from lower strata. | Pierre-Marie Pédrot | |
| 2016-09-15 | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵ | Hugo Herbelin | |
| ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5. | |||
| 2016-09-15 | Continuing fix to #5078, taking also into account intropatterns. | Hugo Herbelin | |
| Getting closer from before when the bug was introduced + test. | |||
| 2016-09-15 | Typo. | Hugo Herbelin | |
| 2016-09-15 | Moving Tactic_matching to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Moving Ltac-specific generic arguments to their own file in the ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Moving Ltac printers to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Generalizing the notion of constr substitution to generic arguments. | Pierre-Marie Pédrot | |
| This removes a dependency on wit_tactic in Constrintern. | |||
| 2016-09-14 | Moving Ltac-specific parsing API to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-14 | Moving the tactic-in-term extension from G_constr to G_ltac. | Pierre-Marie Pédrot | |
| 2016-09-14 | Fix CAMLP4 compilation. | Pierre-Marie Pédrot | |
| 2016-09-14 | Allowing to extend the Print Grammar command generically. | Pierre-Marie Pédrot | |
| We also move the Ltac-specific grammar to its folder. | |||
| 2016-09-14 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-14 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-14 | Fixing test-suite after commit 43104a0b. | Pierre-Marie Pédrot | |
| 2016-09-13 | Fixing #5078 (wrong detection of evaluable local hypotheses). | Hugo Herbelin | |
| 2016-09-13 | LtacProp: fix reset_profile (fix #5079) | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |