aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
* Merge PR#655: Extra functions exported in EConstrGravatar Maxime Dénès2017-05-26
|\
* \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \
| | * | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| * | Merge PR#518: Faster universe unificationGravatar Maxime Dénès2017-05-23
| |\ \
| | | * Exporting some functions of vars.ml as functions operating on EConstr.Gravatar Hugo Herbelin2017-05-19
| | | |
| | | * In EConstr, defining some "cast" functions earlier.Gravatar Hugo Herbelin2017-05-19
| | | | | | | | | | | | | | | | | | | | | | | | This allows to use a cast in subst_of_rel_context_instance. Also added more cast functions for further use.
| | | * Moving "sym" on "eq" type to lib/util.ml.Gravatar Hugo Herbelin2017-05-19
| | |/ | |/|
| * | Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
| |\ \
| * \ \ Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\ \ \
| * | | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | | | |
| | * | | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | | | |
| | * | | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | | | |
| | * | | Add [_] prefix to unused values which maybe should be keptGravatar Gaetan Gilbert2017-04-27
| | | | |
| | * | | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| |/ / /
| | | * Fast path when checking equality of universe levels in UState.Gravatar Pierre-Marie Pédrot2017-04-27
| | | | | | | | | | | | | | | | | | | | We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes.
| | | * Code cleaning in unification algorithm for universes.Gravatar Pierre-Marie Pédrot2017-04-27
| | |/ | |/| | | | | | | | | | | | | | | | This patch is only moving code around and expliciting statically the invariants of the functions, so it should be 1:1 equivalent to the other one. Amongst other goodies, the unification function is not recursive anymore, which ensures that it will terminate.
| * | Fix an optimization failure in tclPROGRESS.Gravatar Pierre-Marie Pédrot2017-04-25
| | | | | | | | | | | | | | | | | | Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails.
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ / | | | | | | Now it is a private field, locations are optional.
* | "tclENV" is sexier, use it instead of "Env.get"Gravatar Matej Kosik2017-04-20
| |
* | reduce syntactic noiseGravatar Matej Kosik2017-04-20
| |
| * Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/ | | | Also remove obvious comments.
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
* | Restore a fast path in EConstr instance normalization.Gravatar Pierre-Marie Pédrot2017-04-01
| |
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | | | The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | For now we only normalize sorts, and we leave instances for the next commit.
* | Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
| |
* | Ensuring proper cast invariants in EConstr.kind.Gravatar Pierre-Marie Pédrot2017-03-31
| | | | | | | | | | | | The kernel does fishy things with casts, such that ensuring there are no two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr view as well.
* | Revert "Specially crafted EConstr.kind to be more efficient."Gravatar Pierre-Marie Pédrot2017-03-31
| | | | | | | | | | This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance difference was not conclusive enough to pay for the code ugliness.
* | Specially crafted EConstr.kind to be more efficient.Gravatar Pierre-Marie Pédrot2017-03-30
| | | | | | | | | | We do one step of loop unrolling, limit the number of allocations and mark the function as inline.
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| | * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| |/ | | | | | | | | | | All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
| * [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself.
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Missing API in EConstr.Gravatar Enrico Tassi2017-02-14
| |
* | Moving evar-normalization functions to EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | This removes code duplication between Evarutil and EConstr.
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
* | Making Evd independent from Namegen.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization.
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | 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.
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | 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
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 08:29:49 +0000