aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2021-02-26Merge PR #13869: Use make_case_or_project in auto_ind_declPierre-Marie Pédrot
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-22Merge PR #13836: Make detyping more resistent in the debuggerPierre-Marie Pédrot
2021-02-17Use make_case_or_project in auto_ind_declGaëtan Gilbert
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
2021-02-08Make detyping more resistent in the debuggerGaëtan Gilbert
2021-01-20Slightly less stupid algorithm for simpl fixpoint expansion.Pierre-Marie Pédrot
2021-01-20Inline the function in contract_[co]fix_use_function.Pierre-Marie Pédrot
2021-01-20Factorize the call of nf_beta in red_elim_const.Pierre-Marie Pédrot
2021-01-20Merge PR #13721: Remove strong reduction wrapperscoqbot-app[bot]
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-18Merge PR #13723: Use a compact case representation for patternscoqbot-app[bot]
2021-01-18Do not call the with_full_binder map variant for Reduction.instance.Pierre-Marie Pédrot
2021-01-18Move the two only calls to the strong combinator to their calling site.Pierre-Marie Pédrot
2021-01-18Move the only use of strong_with_flags to its single calling module.Pierre-Marie Pédrot
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
2021-01-12Same treatment for pattern functions used by rewrite.Pierre-Marie Pédrot
2021-01-12Extrude the check for pattern groundness outside of unification.Pierre-Marie Pédrot
2021-01-12Restore the corner-case behaviour for let-bound variables in patterns.Pierre-Marie Pédrot
2021-01-12Slight tweak of the matching algorithm for PIf vs. Case.Pierre-Marie Pédrot
2021-01-12Change the case representation of patterns.Pierre-Marie Pédrot
2021-01-11Respect print_universes in detype_instanceGaëtan Gilbert
2021-01-04Try to preserve the old unification behaviour w.r.t. let-ins in branches.Pierre-Marie Pédrot
2021-01-04Make detyping more robust w.r.t. case representation.Pierre-Marie Pédrot
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:37:21 +0000