aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2020-11-28Merge PR #13479: extracting API for comparing universes of constants/inductiv...coqbot-app[bot]
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
2020-11-26extracting API for comparing universes of constants/inductives/constructorsbeta
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-25Reserve "sort_expr" for uninterned universesGaëtan Gilbert
2020-11-24Add a new evar source to refer to evars which are types of evars.Hugo Herbelin
2020-11-23Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneousl...Pierre-Marie Pédrot
2020-11-22Fix timeout by ensuring signal exceptions are not erroneously caughtLasse Blaauwbroek
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a primiti...coqbot-app[bot]
2020-11-20Merge PR #13371: Extend hack to use postponed constraints in retyping to temp...coqbot-app[bot]
2020-11-19Use a proper canonical structure entry for projections.Hugo Herbelin
2020-11-19Fixes #9971: expand_projections failing on primitive projections of unknown t...Hugo Herbelin
2020-11-16Merge PR #12873: Unification: A type-checking fix in imitation + an error loc...coqbot-app[bot]
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context of...coqbot-app[bot]
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of...coqbot-app[bot]
2020-11-16Checking type in unification imitation: avoid raising a non-located error.Hugo Herbelin
2020-11-16Fixing a (known) "bugged" part of imitation in unification.Hugo Herbelin
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
2020-11-16Extend hack to use postponed constraints in retyping to template polyGaëtan Gilbert
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ...coqbot-app[bot]
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_...Hugo Herbelin
2020-11-15Locating the Ill-typed evar instance error.Hugo Herbelin
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...coqbot-app[bot]
2020-11-14Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.Hugo Herbelin
2020-11-13Fixes #13363: case of a meta not paying attention to being under binders.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 16:06:43 +0000