| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-23 | Merge PR#518: Faster universe unification | Maxime Dénès | |
| 2017-05-03 | Merge PR#411: Mention template polymorphism in the documentation. | Maxime Dénès | |
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Add [_] prefix to unused values which maybe should be kept | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-27 | Fast path when checking equality of universe levels in UState. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-04-27 | Code cleaning in unification algorithm for universes. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-04-25 | Fix an optimization failure in tclPROGRESS. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-04-25 | [location] Make location optional in Loc.located | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-04-25 | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | |
| Now it is a private field, locations are optional. | |||
| 2017-04-20 | "tclENV" is sexier, use it instead of "Env.get" | Matej Kosik | |
| 2017-04-20 | reduce syntactic noise | Matej Kosik | |
| 2017-04-11 | Update various comments to use "template polymorphism" | Gaetan Gilbert | |
| Also remove obvious comments. | |||
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
| 2017-04-01 | Restore a fast path in EConstr instance normalization. | Pierre-Marie Pédrot | |
| 2017-04-01 | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-04-01 | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | |
| For now we only normalize sorts, and we leave instances for the next commit. | |||
| 2017-03-31 | Make the Constr.kind_of_term type parametric in sorts and universes. | Pierre-Marie Pédrot | |
| 2017-03-31 | Ensuring proper cast invariants in EConstr.kind. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-03-31 | Revert "Specially crafted EConstr.kind to be more efficient." | Pierre-Marie Pédrot | |
| This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance difference was not conclusive enough to pay for the code ugliness. | |||
| 2017-03-30 | Specially crafted EConstr.kind to be more efficient. | Pierre-Marie Pédrot | |
| We do one step of loop unrolling, limit the number of allocations and mark the function as inline. | |||
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-03-23 | Ensuring static invariants about handling of pending evars in Pretyping. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-03-21 | [pp] Remove uses of expensive string_of_ppcmds. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-02-14 | Merge branch 'master'. | Pierre-Marie Pédrot | |
| 2017-02-14 | Missing API in EConstr. | Enrico Tassi | |
| 2017-02-14 | Moving evar-normalization functions to EConstr. | Pierre-Marie Pédrot | |
| This removes code duplication between Evarutil and EConstr. | |||
| 2017-02-14 | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-02-14 | Making Evd independent from Namegen. | Pierre-Marie Pédrot | |
| 2017-02-14 | Moving printing code from Evd to Termops. | Pierre-Marie Pédrot | |
| 2017-02-14 | Chasing a few unsafe constr coercions. | Pierre-Marie Pédrot | |
| 2017-02-14 | Do not ask for a normalized goal to get hypotheses and conclusions. | Pierre-Marie Pédrot | |
| This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization. | |||
| 2017-02-14 | Definining 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-14 | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | |
| 2017-02-14 | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing some return type compatibility layers in Termops. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | |
| 2017-02-14 | Rewrite API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Hints API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Leminv API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Inv API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Contradiction API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Equality API using EConstr. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |