| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-26 | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias | |
| There don't really bring anything, we also correct some minor nits with the printing function. | |||
| 2017-11-24 | Merge PR #486: Make some functions on terms more robust w.r.t new term ↵ | Maxime Dénès | |
| constructs. | |||
| 2017-11-23 | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | |
| 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. | |||
| 2017-11-22 | [api] A few more minor deprecation notices. | Emilio Jesus Gallego Arias | |
| Note the problem with `create_evar_defs`. | |||
| 2017-11-22 | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | |
| 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`. | |||
| 2017-11-21 | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-11-20 | Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵ | Maxime Dénès | |
| unbound rel | |||
| 2017-11-15 | Fix #5761: cbv on undefined evars under binders produces unbound rel | Gaëtan Gilbert | |
| 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. | |||
| 2017-11-13 | [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-08 | Merge PR #922: New beta-iota compatibility refinements | Maxime Dénès | |
| 2017-11-08 | Fixing missing separator in an error message. | Hugo Herbelin | |
| The message is the "Conversion test raised an anomaly" one. | |||
| 2017-11-06 | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | |
| We do up to `Term` which is the main bulk of the changes. | |||
| 2017-11-06 | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | |
| This will allow to merge back `Names` with `API.Names` | |||
| 2017-11-06 | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core. | Maxime Dénès | |
| 2017-11-05 | Refining PR#924 (insensitivity of projection heuristics to alphabet). | Hugo Herbelin | |
| 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). | |||
| 2017-11-04 | [api] Deprecate all legacy uses of Name.Id in core. | Emilio Jesus Gallego Arias | |
| This is a first step towards some of the solutions proposed in #6008. | |||
| 2017-11-03 | Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵ | Maxime Dénès | |
| variables). | |||
| 2017-11-03 | Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵ | Maxime Dénès | |
| alphabet | |||
| 2017-10-28 | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin | |
| This fixes also #5731, #6035, #5364. | |||
| 2017-10-25 | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias | |
| To this extent we factor out the relevant bits to a new file, ltac_pretype. | |||
| 2017-10-17 | 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-09 | Merge PR #1109: Handle some misc todos | Maxime Dénès | |
| 2017-10-03 | Merge PR #1084: After testing it in live, writing metas using an ↵ | Maxime Dénès | |
| ?INTERNAL#42 style is ugly | |||
| 2017-09-29 | Remove some duplication between Typeops and Nativenorm. | Gaëtan Gilbert | |
| 2017-09-28 | 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 | |
| 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). | |||
| 2017-09-26 | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | |
| 2017-09-25 | Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵ | Maxime Dénès | |
| let-ins and non-recursively uniform parameters | |||
| 2017-09-25 | Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵ | Maxime Dénès | |
| 4e70791). | |||
| 2017-09-23 | After testing it in live, writing metas using an ?INTERNAL#42 style is ugly. | Hugo Herbelin | |
| 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). | |||
| 2017-09-23 | 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 | |
| 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". | |||
| 2017-09-22 | Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵ | Maxime Dénès | |
| context obtained by ltac pattern-matching) | |||
| 2017-09-21 | Proposing meta names more distinguishable from evar names than ?M42. | Hugo Herbelin | |
| Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor? | |||
| 2017-09-21 | A possible fix to BZ#5750 (ability to print context of ltac subterm match). | Hugo Herbelin | |
| The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1". | |||
| 2017-09-20 | [flags] Flag `open Flags` | Emilio Jesus Gallego Arias | |
| An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info` | |||
| 2017-09-19 | Merge PR #1036: Unify EConstr.t equality | Maxime Dénès | |
| 2017-09-19 | Allow declaring universe constraints at definition level. | Matthieu Sozeau | |
| Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions. | |||
| 2017-09-15 | Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already. | Maxime Dénès | |
| 2017-09-15 | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès | |
| 2017-09-15 | Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵ | Maxime Dénès | |
| anonymous variables) | |||
| 2017-09-12 | Port is_Set and is_Type to EConstr, as was is_Prop already. | Guillaume Melquiond | |
| 2017-09-08 | Using EConstr equality check in unification. | Pierre-Marie Pédrot | |
| The code from Universes what essentially a duplicate of the one from EConstr, but they were copied for historical reasons. Now, this is not useful anymore, so that we remove the implementation from Universes and rely on the one from EConstr. | |||
| 2017-09-08 | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | |
| When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |