aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: gares Ack-by: ejgallego
2020-10-26Merge 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-21Add missing deprecations in Projection API.Pierre-Marie Pédrot
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce 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-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-10-21Same little game with Projection.Pierre-Marie Pédrot
2020-10-21Deprecate 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-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-19Merge PR #13151: Remove the compare_graph field from the conversion API.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
Reviewed-by: gares
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-14Fix algebraic on the right when using bidi hintsGaë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-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
Reviewed-by: silene
2020-10-13Merge 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-12Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in"coqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-12Catch more errors in Unification.abstract_list_allGaë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-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
Fix #13171
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares
2020-10-11Similarly remove the explicit graph argument in the ~evar conversion API.Pierre-Marie Pédrot
2020-10-11Pick the universe graph out of the environment in conversion API.Pierre-Marie Pédrot
2020-10-11Remove 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-11Fix #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-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-10Adding and using locations on identifiers in constr_expr where they were ↵Hugo Herbelin
missing.
2020-10-09Update pretyping/detyping.mlEnrico Tassi
Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
2020-10-09improve commentEnrico Tassi
2020-10-09No 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-08Dropping 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-07Explicitly 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-07Algorithmically 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-06Remove unused is_class info from cl_contextGaëtan Gilbert
2020-10-06First list in cl_context is just booleansGaëtan Gilbert
Used only by implicit_quantifiers
2020-10-05Wish #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-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-30Further simplification of the typeclass registration API.Pierre-Marie Pédrot
2020-09-30Remove 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.
2020-09-28More precise information when unification fails because of incompatible ↵Hugo Herbelin
candidates. We also show the incompatible contender. Ideally, we should also remember the source of the other contender.
2020-09-03Comment AllowedEvars APIMaxime Dénès
2020-09-02More efficient data structure for allowed evarsMaxime Dénès
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
This is a follow-up of #9062, which introduced a discrenpancy between the two unification engines.
2020-08-31Use a faster algorithm to check for class existence.Pierre-Marie Pédrot
There is a hidden invariant that guarantees that the class index and its reference field are the same.
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: silene
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-08-17Merge PR #12751: Fixes reduction effect printing in the presence of non ↵Pierre-Marie Pédrot
purely applicative stacks Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-08-11Small code simplification in contract_(co)fix.Pierre-Marie Pédrot
Probably a remnant of a time where the difference in code path was relevant.
2020-08-11Move reduce_mind_case from Reductionops to Tacred.Pierre-Marie Pédrot
It was only used there, and its API required to export an ad-hoc type to represent pattern-matchings.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 10:57:07 +0000