aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Collapse)Author
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.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-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Contradiction API using EConstr.Pierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern 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-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-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarsolve 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-11-08Introducing a new EConstr.t type to perform the nf_evar operation on demand.Pierre-Marie Pédrot
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
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.
2016-10-31Stronger static invariant in equality upto universes.Pierre-Marie Pédrot
We return an option type, as constraints were always dropped if the boolean was false. They did not make much sense anyway.
2016-10-31Code factorization in Universes.Pierre-Marie Pédrot
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot
Before this patch, this module was a member of the library folder, which had little to do with its actual use. A tiny part relative to global registering of universe names has been effectively moved to the Global module.
2016-10-30Reordering Termops w.r.t. Evd and Namegen in engine folder.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
Was PR#321: Handling of section variables in hints
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-26COMMENT: Namegen.next_ident_awayMatej Kosik
2016-10-26COMMENT: Proofview.entryMatej Kosik
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-21Oops, my bad, didn't expect a merge issue!Matthieu Sozeau
2016-10-21Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-10-21sections/hints: prevent Not_found in get_type_ofMatthieu Sozeau
due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared.
2016-10-20CLEANUP: Namegen.to_avoidMatej Kosik
This function does the same thing as "Names.Id.List.mem" so: - I deleted the "Namegen.to_avoid" function and - replaced all calls of "Namegen.to_avoid" to calls of "Names.Id.List.mem"
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
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
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-15Fix bug #5145: Anomaly: index to an anonymous variable.Pierre-Marie Pédrot
When printing evar constraints, we ensure that every variable from the rel context has a name.
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 21:50:59 +0000