aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Collapse)Author
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Quote API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Proofview.Goal primitive now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Rewrite API using EConstr.Pierre-Marie Pédrot
2017-02-14Eqdecide API using EConstr.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacticals 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-14Goal 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-14Coercion 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-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-14Nativenorm API using EConstr.Pierre-Marie Pédrot
2017-02-14Vnorm 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-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Merge remote-tracking branch 'git/bug5123' into v8.5Matthieu Sozeau
2016-10-11Fix bug #5123: mark all shelved evars unresolvableMatthieu Sozeau
Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
side_effects. Partial solution to the handling of side effects in proofview.
2016-10-10Fix #4416: - Incorrect "Error: Incorrect number of goals"Arnaud Spiwack
In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-03Merge remote-tracking branch 'github/pr/263' into v8.6Maxime Dénès
Was PR#263: Fast lookup in named contexts
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu Sozeau
This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic.
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-24Moving "move" in the new proof engine.Hugo Herbelin
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-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-16Adding variants enter_one and refine_one which assume that exactly oneHugo Herbelin
goal is under focus and which support returning a relevant output.
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-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-12Merge remote-tracking branch 'github-coq/pr/249' into v8.6Matthieu Sozeau
2016-09-09no-refold patchPaul Steckler
Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
2016-09-09Fast path in Clenvtac.clenv_refine typeclass resolution.Pierre-Marie Pédrot
This legacy function is still used by destruct, and is a hotspot in various examples from the wild. We hijack the check from Typeclass and perform a double check at once not to mark unresolvable evars in vain a lot.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 01:35:41 +0000