index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evd.ml
Commit message (
Expand
)
Author
Age
*
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
*
Sharing identity evar filters.
ppedrot
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
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
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
*
Removing useless evar code.
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
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Optimizing some evar_maps manipulation. In particular, using a [map] instead
ppedrot
2013-09-05
*
Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.
ppedrot
2013-09-05
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
Actually using the domain function for maps.
ppedrot
2013-08-25
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Removing now useless merging primitives from Evd.
ppedrot
2013-08-04
*
Small fixes due to the arrival of OCaml 3.12.
ppedrot
2013-08-03
*
Small cleaning of Evd interface.
ppedrot
2013-05-06
*
Removing a redundant function from Evd.
ppedrot
2013-05-03
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
A version of Univ.check_eq with no anomaly for Evd.set_eq_sort
letouzey
2013-03-12
*
Allowing different types of, not to be mixed, generic Stores through
ppedrot
2013-03-12
*
Locating errors from consider_remaining_unif_problems if possible
herbelin
2013-02-17
*
Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env
herbelin
2013-01-29
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of name
ppedrot
2012-12-18
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Removed some FIXME related to equality on universes.
ppedrot
2012-11-26
*
Small cleaning of interface in Univ
ppedrot
2012-11-26
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
Cleaning and small optimization in CList.
ppedrot
2012-11-20
*
Reversed roles of undefined/defined evars in Evd, thus saving precious
ppedrot
2012-11-03
*
Removed many calls to OCaml generic equality. This was done by
ppedrot
2012-10-29
*
univ inconsistency error message gives evidence of a cycle
barras
2012-10-17
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-15
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Univ: enforce_leq instead of enforce_geq for more uniformity
letouzey
2012-03-22
*
Generalized the use of evar candidates in type inference unification:
herbelin
2012-03-20
*
Noise for nothing
pboutill
2012-03-02
[next]