aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2013-12-06Fix test-suite/success/evars.v.Arnaud Spiwack
2013-12-03Removing useless meta-related functions.Pierre-Marie Pédrot
2013-11-30Better heuristic for name generation backward compatibility. We fallbackPierre-Marie Pédrot
2013-11-30Useless instantiation function exported in Evd.Pierre-Marie Pédrot
2013-11-30Tentative fix to recover fresh name generation as it was beforePierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-25Factoring: is_section_variable.Arnaud Spiwack
2013-11-25Typo resulting in bad eta-expansion of destructing let's body.Hugo Herbelin
2013-11-14Update comments in matching.mli.aspiwack
2013-11-08Removing partial applications in Reductionops.ppedrot
2013-11-07Partial application hunt.ppedrot
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
2013-11-05Preventing useless allocations in Reductionops.instance.ppedrot
2013-11-04Nicer infered names in refine.aspiwack
2013-11-02push_rel_context: do not rename section variables.aspiwack
2013-11-02Fix compilation of pattern matching wrt variables: alias.aspiwack
2013-11-02Fix the compilation of pattern matching wrt to variables.aspiwack
2013-11-02A newly introduced variable inside a named context is no longer α-renamed.aspiwack
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-31Efficient filtered functions in Evd. We test that a filter is actuallyppedrot
2013-10-30Various optimizations of Evd.meta_* functions.ppedrot
2013-10-30More efficient implementation of [Evd.retract_coercible_metas].ppedrot
2013-10-29Optimization in unification: when checking that the head of a term is anppedrot
2013-10-29Useless array-to-list casts in Unification.ppedrot
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
2013-10-29Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.ppedrot
2013-10-29[Reductionops.append_stack_app]: do not allocate a useless array.ppedrot
2013-10-29Sharing identity evar filters.ppedrot
2013-10-29- install evar printer for debuggingmsozeau
2013-10-28Removing Evd.undefined_evars.ppedrot
2013-10-27Removing useless filter allocation in evar construction.ppedrot
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-27Closure optimizations.ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-23Small optimizations in unification.ppedrot
2013-10-23Removing List.mem in Namegen. We may choose a better fitted datastructure tha...ppedrot
2013-10-22Removing some generic equalities.ppedrot
2013-10-22Moving potentially costly computation from exception raising to messageppedrot
2013-10-22Removing useless array-to-list and converse casts used inppedrot
2013-10-22Optimizing evar filters. It seems to cost quite a lot in unification,ppedrot
2013-10-22Various optimizations in Constr, such as term sharing and allocationppedrot
2013-10-08Small code cleaning in Evarutil.ppedrot
2013-10-06Removing useless evar code.ppedrot
2013-10-06Removing uses of Evar.add in class-related functions.ppedrot
2013-10-05Removing dubious use of evarmap manipulating functions in printingppedrot
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 08:00:21 +0000