aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause o...Pierre-Marie Pédrot
2020-11-05Accept section variables in notations with mixed terms and binders.Hugo Herbelin
2020-11-05Fixes #13216 (use of type classes in the return clause of a match).Hugo Herbelin
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
2020-10-31Closes #13278: take into account elimination constraints in small inversion.Hugo Herbelin
2020-10-31Fine-tuning the sort of the predicate obtained by small inversion.Hugo Herbelin
2020-10-31Useless evar type for typing impossible case.Hugo Herbelin
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...coqbot-app[bot]
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
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
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
2020-10-19Merge PR #13151: Remove the compare_graph field from the conversion API.coqbot-app[bot]
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
2020-10-14Fix algebraic on the right when using bidi hintsGaëtan Gilbert
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing tim...Pierre-Marie Pédrot
2020-10-12Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in"coqbot-app[bot]
2020-10-12Check types when converting irrelevant terms in old unificationGaëtan Gilbert
2020-10-12Catch more errors in Unification.abstract_list_allGaëtan Gilbert
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
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
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
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 miss...Hugo Herbelin
2020-10-09Update pretyping/detyping.mlEnrico Tassi
2020-10-09improve commentEnrico Tassi
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
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
2020-10-07Explicitly pass around a state in Evarconv.second_order_matching.Pierre-Marie Pédrot
2020-10-07Algorithmically faster implementation of Evarconv.apply_on_subterm.Pierre-Marie Pédrot
2020-10-06Remove unused is_class info from cl_contextGaëtan Gilbert
2020-10-06First list in cl_context is just booleansGaëtan Gilbert
2020-10-05Wish #12762: warning on duplicated catch-all pattern with unused named variable.Hugo Herbelin
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:59:33 +0000