aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
authorppedrot2012-10-29 13:02:23 +0000
committerppedrot2012-10-29 13:02:23 +0000
commit278517722988d040cb8da822e319d723670ac519 (patch)
tree92316184aec004570c6567f0d585167e47dd52ae /plugins/syntax
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 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions