aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-25Removing useless evar-related stuff.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-18Removing the last global evar generation in Term_dnet. The veryppedrot
2013-09-18Removing unused code from Term_dnet.ppedrot
2013-09-18Removing almost all new_untyped_evar, and a bunch of Evd.add.ppedrot
2013-09-18Taming the simpl evar hack that used to use negative evars.ppedrot
2013-09-12Unplugging Autoinstance. The code is still here if someone wishesppedrot
2013-09-05Optimizing some evar_maps manipulation. In particular, using a [map] insteadppedrot
2013-09-05Documentation of Evd.ppedrot
2013-09-05Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.ppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-25Removing association lists in Reductionops. Btw, defining the dual of theppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 04:48:15 +0000