aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
AgeCommit message (Expand)Author
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06Restore reasonable performance by not allocating during universe checks,Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-11Made Pre_env.lazy_val opaque.Pierre-Marie Pédrot
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-01-29Using Map.smartmap whenever deemed useful.Pierre-Marie Pédrot
2014-01-07STM: additional fix for STM + vm_computeEnrico Tassi
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-30Tentative fix to recover fresh name generation as it was beforePierre-Marie Pédrot
2013-11-25Factoring: is_section_variable.Arnaud Spiwack
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
2013-11-04Nicer infered names in refine.aspiwack
2013-11-02push_rel_context: do not rename section variables.aspiwack
2013-11-02A newly introduced variable inside a named context is no longer α-renamed.aspiwack
2013-10-29Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.ppedrot
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-22Removing some generic equalities.ppedrot
2013-10-22Optimizing evar filters. It seems to cost quite a lot in unification,ppedrot
2013-10-08Small code cleaning in Evarutil.ppedrot
2013-10-06Removing useless evar code.ppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-18Removing almost all new_untyped_evar, and a bunch of Evd.add.ppedrot
2013-09-05Optimizing some evar_maps manipulation. In particular, using a [map] insteadppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-25Actually using the domain function for maps.ppedrot
2013-08-25Replacing lists by sets in clear tactic.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
2013-02-10Splitted Evarutil in two filesppedrot
2013-02-10Moved code from Pretype_error to Evarutilppedrot
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Fixing one part of #2830 (anomaly "defined twice" due to nested calls toherbelin
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-25Fixed bug #2930: folded let-in's were hiding a violation to the occurherbelin
2012-11-22Monomorphization (pretyping)ppedrot
2012-11-20Cleaning and small optimization in CList.ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 20:47:01 +0000