| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-13 | Make the universe of primitive arrays irrelevant | Gaëtan Gilbert | |
| Fix #13354 This change is very specific to array, but should not be a significant obstacle to generalization of the feature to eg axioms if we want to later. | |||
| 2020-11-12 | Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ↵ | Pierre-Marie Pédrot | |
| naming Ack-by: gares Reviewed-by: ppedrot | |||
| 2020-11-09 | Remove the native symbol registering from the safe environment. | Pierre-Marie Pédrot | |
| Instead we store that data in the native code that was generated in adapt the compilation scheme accordingly. Less indirections and less imperative tinkering makes the code safer. The global symbol table was originally introduced in #10359 as a way not to depend on the Global module in the generated code. By storing all the native-related information in the cmxs file itself, this PR also makes other changes easier, such as e.g. #13287. | |||
| 2020-11-09 | Merge PR #13217: Addresses #13216: use of type classes in the return clause ↵ | Pierre-Marie Pédrot | |
| of a match. Reviewed-by: ppedrot | |||
| 2020-11-05 | Accept section variables in notations with mixed terms and binders. | Hugo Herbelin | |
| 2020-11-05 | Fixes #13216 (use of type classes in the return clause of a match). | Hugo Herbelin | |
| This was deactivated in fb1c2a017e but it seems useful (e.g. in contribs containers). It seems to be useful | |||
| 2020-11-05 | Merge PR #13182: Check types when converting irrelevant terms in old unification | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-11-04 | Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming. | Hugo Herbelin | |
| Also some dead code. If no typo is introduced, there should be no semantic changes. | |||
| 2020-10-31 | Closes #13278: take into account elimination constraints in small inversion. | Hugo Herbelin | |
| Ideally, if equations t <= ?x were preserving subtyping that could be simpler. Currently we need however to put a rigid universe as constraint on the return predicate so that one branch does not force the return sort to be lower by unification than what another branch would have needed. | |||
| 2020-10-31 | Fine-tuning the sort of the predicate obtained by small inversion. | Hugo Herbelin | |
| If the result is in SProp, Prop or (impredicative) Set, we preserve this information since the elimination sort might be restricted by the sort of the destructed type. If the result is in Type, we use a fresh sort upper bound so that we are sure not having residual algebraic universes which would raise problems in a type constraint (e.g. in define_evar_as_product). This fixes the part of #13278 posted on discourse. | |||
| 2020-10-31 | Useless evar type for typing impossible case. | Hugo Herbelin | |
| 2020-10-27 | Merge PR #13075: Introducing the foundations for a name-alias-agnostic API | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: gares Ack-by: ejgallego | |||
| 2020-10-26 | Merge PR #12768: Granting wish #12762: warning on duplicated catch-all ↵ | coqbot-app[bot] | |
| pattern-matching clause with unused named variable Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares | |||
| 2020-10-21 | Add missing deprecations in Projection API. | Pierre-Marie Pédrot | |
| 2020-10-21 | Similar introduction of a Construct module in the Names API. | Pierre-Marie Pédrot | |
| 2020-10-21 | Introduce an Ind module in the Names API. | Pierre-Marie Pédrot | |
| This is similar to Constant and MutInd but for some reason this was was never done. Such a patch makes the whole API more regular. We also deprecate the legacy aliases. | |||
| 2020-10-21 | Rename the GlobRef comparison modules following the standard pattern. | Pierre-Marie Pédrot | |
| 2020-10-21 | Same little game with Projection. | Pierre-Marie Pédrot | |
| 2020-10-21 | Deprecate the non-qualified equality functions on kerpairs. | Pierre-Marie Pédrot | |
| This allows to quickly spot the parts of the code that rely on the canonical ordering. When possible we directly introduce the quotient-aware versions. | |||
| 2020-10-21 | Merge PR #13118: [type classes] Simplify cl_context | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-10-19 | Merge PR #13151: Remove the compare_graph field from the conversion API. | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2020-10-19 | Merge PR #13192: Fix algebraic on the right when using bidi hints | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-10-15 | Merge PR #13181: Guard unify_leq_delay calls in Typing | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-10-14 | Fix algebraic on the right when using bidi hints | Gaëtan Gilbert | |
| Fix #12970 We can't recover the expected type of the post bidi argument by retyping because the hole may be filled by something in which case retyping can produce algebraic universes. | |||
| 2020-10-13 | Merge PR #13172: Fix #13169: vm_compute has existential crisis. | coqbot-app[bot] | |
| Reviewed-by: silene | |||
| 2020-10-13 | Merge PR #13099: Locating pattern identifiers (?id) by default at parsing ↵ | Pierre-Marie Pédrot | |
| time and use location in some typing error messages Reviewed-by: ppedrot | |||
| 2020-10-12 | Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in" | coqbot-app[bot] | |
| Reviewed-by: herbelin Ack-by: SkySkimmer | |||
| 2020-10-12 | Check types when converting irrelevant terms in old unification | Gaëtan Gilbert | |
| Fixes probably many strange issues such as the example in #13171 | |||
| 2020-10-12 | Catch more errors in Unification.abstract_list_all | Gaëtan Gilbert | |
| This improves the error message on the example for #13171, however we may question whether there should be an error at all. | |||
| 2020-10-12 | Guard unify_leq_delay calls in Typing | Gaëtan Gilbert | |
| Fix #13171 | |||
| 2020-10-12 | Merge PR #12449: Minimize Prop <= i to i := Set | coqbot-app[bot] | |
| Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares | |||
| 2020-10-11 | Similarly remove the explicit graph argument in the ~evar conversion API. | Pierre-Marie Pédrot | |
| 2020-10-11 | Pick the universe graph out of the environment in conversion API. | Pierre-Marie Pédrot | |
| 2020-10-11 | Remove the compare_graph field from the conversion API. | Pierre-Marie Pédrot | |
| We know statically that the first thing the conversion algorithm is going to do is to get it from the provided function, so we simply explicitly pass it around. | |||
| 2020-10-11 | Fix #13169: vm_compute has existential crisis. | Pierre-Marie Pédrot | |
| We simply use evars instance in the right order while reading back VM values. | |||
| 2020-10-10 | Add location in existential variable names (CEvar/GEvar). | Hugo Herbelin | |
| 2020-10-10 | Adding and using locations on identifiers in constr_expr where they were ↵ | Hugo Herbelin | |
| missing. | |||
| 2020-10-09 | Update pretyping/detyping.ml | Enrico Tassi | |
| Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com> | |||
| 2020-10-09 | improve comment | Enrico Tassi | |
| 2020-10-09 | No bidirectionality when expected type for lambda is an evar. | Gaëtan Gilbert | |
| This fixes #12623 (bidirectionality breaks impredicativity). | |||
| 2020-10-09 | [printing] make detyping resilient to "let x : _ := t in" | Enrico Tassi | |
| 2020-10-08 | Dropping the misleading int argument of Pp.h. | Hugo Herbelin | |
| An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended. | |||
| 2020-10-07 | Explicitly pass around a state in Evarconv.second_order_matching. | Pierre-Marie Pédrot | |
| I know higher-order mutable state shared across call sites is a staple of Matthieu's style, but it is a footgun begging to be abused. | |||
| 2020-10-07 | Algorithmically faster implementation of Evarconv.apply_on_subterm. | Pierre-Marie Pédrot | |
| Instead of repeatedly checking for evars to appear in a term, we perform the search in one single pass. This slowdown was observed in fiat-crypto. This is still a naive algorithm though, since we recompute the set of evars for each subterm. This is thus quadratic. | |||
| 2020-10-06 | Remove unused is_class info from cl_context | Gaëtan Gilbert | |
| 2020-10-06 | First list in cl_context is just booleans | Gaëtan Gilbert | |
| Used only by implicit_quantifiers | |||
| 2020-10-05 | Wish #12762: warning on duplicated catch-all pattern with unused named variable. | Hugo Herbelin | |
| An identifier starting with _ deactivates the warning. Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2020-10-02 | Merge PR #13106: Remove the forward class hint feature. | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2020-09-30 | Further simplification of the typeclass registration API. | Pierre-Marie Pédrot | |
| 2020-09-30 | Remove the forward class hint feature. | Pierre-Marie Pédrot | |
| It was not documented, not properly tested and thus likely buggy. Judging from the code alone I spotted already one potential bug. Further more it was prominently making use of the infamous "arbitrary term as hint" feature. Since the only user in our CI seems to be a math-classes file that introduced the feature under a claim of "cleanup", I believe we can safely remove it without anyone noticing. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |