index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Removing partial applications in Reductionops.
ppedrot
2013-11-08
*
Partial application hunt.
ppedrot
2013-11-07
*
Less partial applications in Vars, as well as better memory allocation.
ppedrot
2013-11-06
*
Preventing useless allocations in Reductionops.instance.
ppedrot
2013-11-05
*
Nicer infered names in refine.
aspiwack
2013-11-04
*
push_rel_context: do not rename section variables.
aspiwack
2013-11-02
*
Fix compilation of pattern matching wrt variables: alias.
aspiwack
2013-11-02
*
Fix the compilation of pattern matching wrt to variables.
aspiwack
2013-11-02
*
A newly introduced variable inside a named context is no longer α-renamed.
aspiwack
2013-11-02
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
Efficient filtered functions in Evd. We test that a filter is actually
ppedrot
2013-10-31
*
Various optimizations of Evd.meta_* functions.
ppedrot
2013-10-30
*
More efficient implementation of [Evd.retract_coercible_metas].
ppedrot
2013-10-30
*
Optimization in unification: when checking that the head of a term is an
ppedrot
2013-10-29
*
Useless array-to-list casts in Unification.
ppedrot
2013-10-29
*
Do not generate useless argument arrays in whd_* functions.
ppedrot
2013-10-29
*
Prevent [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-29
*
Sharing identity evar filters.
ppedrot
2013-10-29
*
- install evar printer for debugging
msozeau
2013-10-29
*
Removing Evd.undefined_evars.
ppedrot
2013-10-28
*
Removing useless filter allocation in evar construction.
ppedrot
2013-10-27
*
Abstracting evar filter away. The API is not perfect, but better than nothing.
ppedrot
2013-10-27
*
Closure optimizations.
ppedrot
2013-10-27
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
cList: a few alternative to hashtbl-based uniquize, distinct, subset
letouzey
2013-10-23
*
cList.index is now cList.index_f, same for index0
letouzey
2013-10-23
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
Small optimizations in unification.
ppedrot
2013-10-23
*
Removing List.mem in Namegen. We may choose a better fitted datastructure tha...
ppedrot
2013-10-23
*
Removing some generic equalities.
ppedrot
2013-10-22
*
Moving potentially costly computation from exception raising to message
ppedrot
2013-10-22
*
Removing useless array-to-list and converse casts used in
ppedrot
2013-10-22
*
Optimizing evar filters. It seems to cost quite a lot in unification,
ppedrot
2013-10-22
*
Various optimizations in Constr, such as term sharing and allocation
ppedrot
2013-10-22
*
Small code cleaning in Evarutil.
ppedrot
2013-10-08
*
Removing useless evar code.
ppedrot
2013-10-06
*
Removing uses of Evar.add in class-related functions.
ppedrot
2013-10-06
*
Removing dubious use of evarmap manipulating functions in printing
ppedrot
2013-10-05
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Removing useless evar-related stuff.
ppedrot
2013-09-25
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Removing the last global evar generation in Term_dnet. The very
ppedrot
2013-09-18
*
Removing unused code from Term_dnet.
ppedrot
2013-09-18
*
Removing almost all new_untyped_evar, and a bunch of Evd.add.
ppedrot
2013-09-18
*
Taming the simpl evar hack that used to use negative evars.
ppedrot
2013-09-18
*
Unplugging Autoinstance. The code is still here if someone wishes
ppedrot
2013-09-12
[next]