aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
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.
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-08-06Use the evarinfo-stored identity substitution where applicable.Pierre-Marie Pédrot
2020-07-24Fixes reduction effect printing in the presence of non purely applicative ↵Hugo Herbelin
stacks.
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
No need to store the case_info, all the data is reconstructible from the context. Furthermore, this reconstruction is performed in a context where we already access the environment, so performance is not at stake. Hopefully this will also reduce the number of globally allocated VM values, since the switch representation now only depends on the shape of the inductive type.
2020-07-18Merge PR #12588: [exn] Remove some uses of printPierre-Marie Pédrot
Ack-by: gares Reviewed-by: ppedrot
2020-07-13Don't catch anomalies for evarconv "cannot find an instance" errorGaëtan Gilbert
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject ↵Pierre-Marie Pédrot
entry struc_tuple Reviewed-by: ppedrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-10Merge PR #12638: Some changes of representation in TacredEnrico Tassi
Ack-by: backtracking Reviewed-by: gares
2020-07-09[error handling] Anomaly in Conversion is a "precatchable_exception"Emilio Jesus Gallego Arias
This is just a fixup, likely all the places that are matching on `UserErr` directly are just buggy.
2020-07-09[reductionops] Comment about absorption of anomalies.Emilio Jesus Gallego Arias
Co-authored-by: <Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
2020-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
Exceptions should not printed except for the top-level. There is the weird anomaly-absorbing code in `Reductionops`, I wonder how frequent that case is, but as the exception is absorbed printing there could have a real impact.
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
This requires updating the parameter count at section end, I felt it was easier to do with rebuild_function but it could be done in discharge if needed. Incidentally fixes #12649.
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive ↵Enrico Tassi
projection Reviewed-by: ejgallego Ack-by: gares
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 20:49:55 +0000