aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorppedrot2012-10-29 13:02:23 +0000
committerppedrot2012-10-29 13:02:23 +0000
commit278517722988d040cb8da822e319d723670ac519 (patch)
tree92316184aec004570c6567f0d585167e47dd52ae /kernel/type_errors.ml
parent0699ef2ffba984e7b7552787894b142dd924f66a (diff)
Removed many calls to OCaml generic equality. This was done by
writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions