aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-12-21Remove the artificial dependency of Heads on evaluable_global_reference.Pierre-Marie Pédrot
2020-12-20Merge PR #13138: Towards a documentation / cleanup of evarconvcoqbot-app[bot]
2020-12-18Merge PR #13628: Cache meta instances in Clenvcoqbot-app[bot]
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ta...Pierre-Marie Pédrot
2020-12-15Merge PR #13625: Tweak constr_matching so as to make it tail-rec on projectio...coqbot-app[bot]
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
2020-12-14Do not rely on Reductionops to recognize canonical projections.Pierre-Marie Pédrot
2020-12-14Remove most of Reductionops.*_state functions.Pierre-Marie Pédrot
2020-12-14Cache meta access in meta_instance.Pierre-Marie Pédrot
2020-12-12Tweak constr_matching so as to make it tail-rec on projection expansion.Pierre-Marie Pédrot
2020-12-11Removing non relevant argument binding_kind of GLocalDef.Hugo Herbelin
2020-12-10Merge PR #12100: Fixing use of argument scopes in patterns + a further cleanu...coqbot-app[bot]
2020-12-09Optimization: take advantage that we don't use arrays anymore in substitutions.Pierre-Marie Pédrot
2020-12-09Using self-documenting argument names in two exceptions of cases.ml.Hugo Herbelin
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
2020-12-09Adding functions to returning the def/decl status of an inductive arity.Hugo Herbelin
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-21More documentation about the situation ?ev := C[?ev'] in solve_simple_eqn.Hugo Herbelin
2020-11-21Unification: renamings in ise_stack2 to get a more explicit idea of its seman...Hugo Herbelin
2020-11-21Some partial documentation of evar_conv_x.Hugo Herbelin
2020-11-21Short documentation of solve_simple_eqn.Hugo Herbelin
2020-11-21Documenting module Reductionops.Stack.Hugo Herbelin
2020-11-21Unification: documenting eta for pi-types and record types.Hugo Herbelin
2020-11-21Deduce Stack.decomp from Stack.strip_n_app.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:06:37 +0000