| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-26 | Add a compatibility flag for 8.6 and refactor. | Théo Zimmermann | |
| 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 | Further "decide equality" tests on demand of Jason. | Hugo Herbelin | |
| 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 | |
| 2016-09-13 | test-suite/output-modulo-time made more robust | Enrico Tassi | |
| 2016-09-13 | AsyncTaskQueue: annotate debug feedback messages with worker id | Enrico Tassi | |
| 2016-09-13 | CoqIDE: push to message win feedback Message(Debug,Info,Notice) | Enrico Tassi | |
| 2016-09-13 | coqc: print debug feedback coming from workers | Enrico Tassi | |
| This way par:eauto and all:eato print the same debugging traecs | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |