aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
* Merge PR#393: Replace Typeops with Fast_typeopsGravatar Maxime Dénès2017-02-08
|\
* | Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
* | Extraction cosmetic: no whitespaces in printing empty modulesGravatar Pierre Letouzey2017-02-07
| |
* | Extraction: remove the "print to devnull" hack now that pp isn't lazy anymoreGravatar Pierre Letouzey2017-02-07
| |
* | Extraction: avoid deprecated functions of module StringGravatar Pierre Letouzey2017-02-07
| | | | | | | | | | - A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co
* | Extraction: simplify the generated code for difficult name conflictsGravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | No more pp_alias_spec et pp_alias_decl. Instead, we use "include" and "module type of". The extracted code might hence need OCaml 3.12 (quite rarely)
* | Extraction : get_duplicates (via option) instead of check_duplicates (via ↵Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | Not_found) This clarifies the execution flow
* | Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
| * Remove useless commentsGravatar Gaetan Gilbert2017-01-28
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \
| | * Extend Fast_typeops to be a replacement for TypeopsGravatar Gaetan Gilbert2016-12-12
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This brings the fix in cad44fc for #2996 to the copy of Fast_typeops.check_hyps_inclusion. Fast_typeops.constant_type checks the universe constraints instead of outputting them. Since everyone who used Typeops.constant_type just discarded the constraints they've been switched to constant_type_in which should be the same in Fast_typeops and Typeops. There are some small differences in the interfaces: - Typeops.type_of_projection <-> Fast_typeops.type_of_projection_constant to avoid collision with the internally used type_of_projection (which gives the type of [Proj(p,c)]). - check_hyps_inclusion takes [('a -> constr)] and ['a] instead of [constr] for reporting errors.
| * ssrmatching: fix iter_constr_LR iterator wrt ProjGravatar Enrico Tassi2016-12-07
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\|
| * ssrmatching: handle primite projections (fix: #5247)Gravatar Enrico Tassi2016-12-05
| |
| * Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-12-02
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * Lazily load constants in micromega (bug #5134).Gravatar Guillaume Melquiond2016-11-24
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ | | | | | | | | | Was PR#331: Solve_constraints and Set Use Unification Heuristics
* | | Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
| | | | | | | | | | | | | | | | | | | | | Strangely enough, the checker seems to rely on an outdated decompose_app function which is not the same as the kernel, as the latter is sensitive to casts. Cast-manipulating functions from the kernel are only used on upper layers, and thus was moved there.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| |
| * | Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ | | | | | | | | | | | | Was PR#319: More error tagging, try to fix bug 5135
| * \ \ Merge commit 'a799600' into v8.6Gravatar Maxime Dénès2016-10-25
| |\ \ \ | | | | | | | | | | | | | | | Was PR#334: Fix bug 5031 : should not be an anomaly
| | * | | That Function is unable to create a Fixpoint equation is a user problem,Gravatar Yves Bertot2016-10-25
| | | | | | | | | | | | | | | | | | | | not an anomaly
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | | |
| * | | | ssrmatching: fix interpretation of rpatternGravatar Enrico Tassi2016-10-24
| |/ / /
| | | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |/ | |/| | | | | | | | | | reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
* | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
| | | | | | | | | | | | | | | | | | | | | The word "increment" is more appropriate in this case than "lifting". The world "lifting", in computer science, usually denotes something else: https://en.wikipedia.org/wiki/Lambda_lifting
| | * [pp] Use more convenient pp API in ssrmatchingGravatar Emilio Jesus Gallego Arias2016-10-18
| | |
| | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |/ | | | | | | | | | | | | | | The current tag system in `Pp` is generic, which implies we must choose a tagging function when calling a printer. For console printing there is a single choice, thus this commits adds it a few missing cases.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Fix bug #5023: JSON extraction doesn't generate "for xxx".Gravatar Pierre-Marie Pédrot2016-10-17
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Ncring_initial: avoid a notation overridingGravatar Pierre Letouzey2016-09-29
| |
| * Extraction: ignore some useless stuff about universesGravatar Pierre Letouzey2016-09-29
| |
| * Ring_theory: avoid overriding a few notationsGravatar Pierre Letouzey2016-09-28
| |
| * Adding interface files to Nsatz ML files.Gravatar Pierre-Marie Pédrot2016-09-28
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\|
| * Fast russian peasant exponentiation in Nsatz.Gravatar Pierre-Marie Pédrot2016-09-26
| |
| * Monomorphizing various uses of arrays in Nsatz.Gravatar Pierre-Marie Pédrot2016-09-26
| |
| * Partial fix for bug #5085: nsatz_compute stack overflows.Gravatar Pierre-Marie Pédrot2016-09-26
| | | | | | | | | | This fixes the stack overflow part of the bug, even if the tactic is still quite slow. The offending functions have been written in a tail-recursive way.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
| | | | | | | | | | | | | | | | | | 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.
* | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \ | | | | | | | | | Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
* | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| | | | | | | | | | | | | | | | | | 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.
| * | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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".
| * Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
| | | | | | | | One of them revealed a true bug.
* | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 00:58:36 +0000