aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
* Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
|
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | 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.
* Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Introducing a new EConstr.t type to perform the nf_evar operation on demand.Gravatar Pierre-Marie Pédrot2016-11-08
|
* 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.
* Stronger static invariant in equality upto universes.Gravatar Pierre-Marie Pédrot2016-10-31
| | | | | We return an option type, as constraints were always dropped if the boolean was false. They did not make much sense anyway.
* Code factorization in Universes.Gravatar Pierre-Marie Pédrot2016-10-31
|
* Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
| | | | | | 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.
* Reordering Termops w.r.t. Evd and Namegen in engine folder.Gravatar Pierre-Marie Pédrot2016-10-30
|
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * Merge remote-tracking branch 'github/pr/321' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ | | | | | | | | | Was PR#321: Handling of section variables in hints
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| | |
* | | COMMENT: Namegen.next_ident_awayGravatar Matej Kosik2016-10-26
| | |
* | | COMMENT: Proofview.entryGravatar Matej Kosik2016-10-26
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| |
| * | Oops, my bad, didn't expect a merge issue!Gravatar Matthieu Sozeau2016-10-21
| | |
| * | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
| | |
| | * sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
| |/ | | | | | | | | | | | | | | 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.
* | CLEANUP: Namegen.to_avoidGravatar Matej Kosik2016-10-20
| | | | | | | | | | | | 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"
* | 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
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Fix bug #5145: Anomaly: index to an anonymous variable.Gravatar Pierre-Marie Pédrot2016-10-15
| | | | | | | | | | When printing evar constraints, we ensure that every variable from the rel context has a name.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| |
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
| |\ | | | | | | | | | Was PR#263: Fast lookup in named contexts
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 21:26:23 +0000