Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #6338: Remove up-to-conversion term matching | Maxime Dénès | 2017-12-11 |
|\ | |||
| * | Remove up-to-conversion matching functions. | Pierre-Marie Pédrot | 2017-12-09 |
| | | | | | | | | They were not used anymore since the previous patches. | ||
* | | Getting rid of the Update constructor in Reductionops. | Pierre-Marie Pédrot | 2017-12-06 |
| | | | | | | | | | | This was dead code, probably due to the fact it was once shared with the kernel stack type. | ||
* | | Getting rid of the Shift constructor in Reductionops. | Pierre-Marie Pédrot | 2017-12-06 |
|/ | | | | | It was actually not used. The only place generating one was easily writable without it. | ||
* | Proper nametab handling of global universe names | Matthieu Sozeau | 2017-12-01 |
| | | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced | ||
* | Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵ | Maxime Dénès | 2017-11-30 |
|\ | | | | | | | #3125) | ||
| * | Adding a variant get_truncation_family_of of get_sort_family_of. | Hugo Herbelin | 2017-11-28 |
| | | | | | | | | | | | | | | | | | | This function returns InProp or InSet for inductive types only when the inductive type has been explicitly truncated to Prop or (impredicative) Set. For instance, singleton inductive types and small (predicative) inductive types are not truncated and hence in Type. | ||
| * | Moving non-recursive function sort_family_of out of the retype block of ↵ | Hugo Herbelin | 2017-11-28 |
| | | | | | | | | recursive functions. | ||
* | | Merge PR #1033: Universe binder improvements | Maxime Dénès | 2017-11-28 |
|\ \ | |||
* | | | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias | 2017-11-26 |
| |/ |/| | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function. | ||
| * | Fix interpretation of global universes in univdecl constraints. | Gaëtan Gilbert | 2017-11-25 |
| | | | | | | | | Also nicer error when the constraints are impossible. | ||
| * | Use Maps and ids for universe binders | Gaëtan Gilbert | 2017-11-24 |
|/ | | | | Before sometimes there were lists and strings. | ||
* | Merge PR #486: Make some functions on terms more robust w.r.t new term ↵ | Maxime Dénès | 2017-11-24 |
|\ | | | | | | | constructs. | ||
| * | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | 2017-11-23 |
| | | | | | | | | | | | | Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings. | ||
* | | [api] A few more minor deprecation notices. | Emilio Jesus Gallego Arias | 2017-11-22 |
| | | | | | | | | Note the problem with `create_evar_defs`. | ||
* | | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | 2017-11-22 |
| | | | | | | | | | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`. | ||
* | | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias | 2017-11-21 |
|/ | | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization. | ||
* | Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵ | Maxime Dénès | 2017-11-20 |
|\ | | | | | | | unbound rel | ||
| * | Fix #5761: cbv on undefined evars under binders produces unbound rel | Gaëtan Gilbert | 2017-11-15 |
| | | | | | | | | | | | | | | When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case. | ||
* | | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | 2017-11-13 |
|/ | |||
* | Merge PR #6098: [api] Move structures deprecated in the API to the core. | Maxime Dénès | 2017-11-13 |
|\ | |||
* \ | Merge PR #6117: Fix printing anomaly in conv | Maxime Dénès | 2017-11-13 |
|\ \ | |||
* \ \ | Merge PR #6065: [api] Deprecate all legacy uses of Names in core. | Maxime Dénès | 2017-11-13 |
|\ \ \ | |||
* \ \ \ | Merge PR #922: New beta-iota compatibility refinements | Maxime Dénès | 2017-11-08 |
|\ \ \ \ | |||
| | | * | | Fixing missing separator in an error message. | Hugo Herbelin | 2017-11-08 |
| |_|/ / |/| | | | | | | | | | | | The message is the "Conversion test raised an anomaly" one. | ||
| | | * | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | 2017-11-06 |
| | |/ | | | | | | | | | | We do up to `Term` which is the main bulk of the changes. | ||
| | * | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | 2017-11-06 |
| |/ |/| | | | | | This will allow to merge back `Names` with `API.Names` | ||
* | | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core. | Maxime Dénès | 2017-11-06 |
|\ \ | |||
* | | | Refining PR#924 (insensitivity of projection heuristics to alphabet). | Hugo Herbelin | 2017-11-05 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed). | ||
| * | | [api] Deprecate all legacy uses of Name.Id in core. | Emilio Jesus Gallego Arias | 2017-11-04 |
|/ / | | | | | | | This is a first step towards some of the solutions proposed in #6008. | ||
* | | Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵ | Maxime Dénès | 2017-11-03 |
|\ \ | | | | | | | | | | variables). | ||
* \ \ | Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵ | Maxime Dénès | 2017-11-03 |
|\ \ \ | | | | | | | | | | | | | alphabet | ||
| | * | | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin | 2017-10-28 |
| |/ / |/| | | | | | | | | This fixes also #5731, #6035, #5364. | ||
* | | | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias | 2017-10-25 |
| | | | | | | | | | | | | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype. | ||
* | | | unification: fix BZ#5692, recognize prim projs as CS projections | Matthieu Sozeau | 2017-10-17 |
| | | | |||
* | | | Properly handling projection parameters in canonical structures. | Pierre-Marie Pédrot | 2017-10-17 |
| | | | |||
* | | | Handling primitive projections in canonical structures. | Pierre-Marie Pédrot | 2017-10-17 |
| | | | |||
* | | | Merge PR #1109: Handle some misc todos | Maxime Dénès | 2017-10-09 |
|\ \ \ | |||
* \ \ \ | Merge PR #1084: After testing it in live, writing metas using an ↵ | Maxime Dénès | 2017-10-03 |
|\ \ \ \ | | | | | | | | | | | | | | | | ?INTERNAL#42 style is ugly | ||
| | * | | | Remove some duplication between Typeops and Nativenorm. | Gaëtan Gilbert | 2017-09-29 |
| | | | | | |||
| | * | | | Remove trivial TODO comment (constants can't be template poly now). | Gaëtan Gilbert | 2017-09-28 |
| | | | | | |||
* | | | | | Efficient computation of the names contained in an environment. | Pierre-Marie Pédrot | 2017-09-28 |
| | | | | | |||
* | | | | | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | 2017-09-28 |
| |/ / / |/| | | | | | | | | | | | | | | | The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n). | ||
* | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | 2017-09-26 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵ | Maxime Dénès | 2017-09-25 |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | let-ins and non-recursively uniform parameters | ||
* \ \ \ \ \ | Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵ | Maxime Dénès | 2017-09-25 |
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | 4e70791). | ||
| | | | * | | | After testing it in live, writing metas using an ?INTERNAL#42 style is ugly. | Hugo Herbelin | 2017-09-23 |
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Printing metas still happens relatively often. From the user point of view, no need to know that it is different from an evar, so the notation ?M42 as it was before is much lighter. As for developers looking for debugging information, they will easily suspect that it is internally a meta because of the "M". This reverts "Proposing meta names more distinguishable from evar names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead). | ||
| * | | | | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791). | Hugo Herbelin | 2017-09-23 |
| | | | | | | |||
| | * | | | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params. | Hugo Herbelin | 2017-09-23 |
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop". | ||
* | | | | | Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵ | Maxime Dénès | 2017-09-22 |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | context obtained by ltac pattern-matching) |