aboutsummaryrefslogtreecommitdiff
path: root/ltac
AgeCommit message (Collapse)Author
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Refine API using EConstr.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Typeclasses API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2017-02-14Constr_matching API using EConstr.Pierre-Marie Pédrot
2017-02-14Patternops API using EConstr.Pierre-Marie Pédrot
2017-02-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-29Fixing #5164 (regression in locating error in argument of "refine").Hugo Herbelin
Reporting location was not expecting a term passed to an ML tactic to be interpreted by the ML tactic itself. Made an empirical fix to report about the as-precise-as-possible location available.
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-22Merge branch 'v8.5' into v8.6Hugo Herbelin
2016-10-21Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Matthieu Sozeau
This makes [refine] typecheck the term only once (instead of twice), (Qed excluded of course). Fix test-suite file for output of constraints accordingly.
2016-10-20Merge branch 'bug5036' into v8.6Matthieu Sozeau
2016-10-20Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Fix bug #5116: [Print Ltac] should be able to print strategies.Pierre-Marie Pédrot
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-08Fix bug #5098: Symmetry broken in HoTT.Pierre-Marie Pédrot
We defactorize the in_clause grammar entry to allow parsing of the "symmetry" tactic when it has no arguments. Beforehand, the clause_dft_concl entry accepted the empty stream, preventing the definition of symmetry as a mere identifier.
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-29LtacProf cutoff is for total percent, not timeJason Gross
2016-09-29Merge branch 'bug5036' into v8.6Matthieu Sozeau
2016-09-29Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
2016-09-29-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)Enrico Tassi
With this command line flag one can profile ltac in files /and/ trim the results without actually touching the files.
2016-09-28Merge remote-tracking branch 'github/pr/232' into v8.6Maxime Dénès
Was PR#232: Fix the parsing of goal selectors.
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-27LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)Enrico Tassi
It seems we have no grammar rule that parses floats, so I'm parsing an integer, but the whole machinery supports floats.
2016-09-26Fix bug #5093: typeclasses eauto depth arg does not accept a var.Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-22Revert "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-22Merge remote-tracking branch 'github/pr/283' into trunkMaxime Dénès
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
2016-09-21Merging 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-20Stylistic 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-16Make 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-15Moving Tacexpr to ltac/ folder.Pierre-Marie Pédrot
2016-09-15Made Ppanotation Ltac-agnostic.Pierre-Marie Pédrot
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-09-15Continuing fix to #5078, taking also into account intropatterns.Hugo Herbelin
Getting closer from before when the bug was introduced + test.
2016-09-15Moving Tactic_matching to ltac/ folder.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 00:36:26 +0000