diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-31 00:45:45 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-31 00:45:45 +0000 |
| commit | b0631cba10fda88eb3518153860807b10441ef34 (patch) | |
| tree | bd1da0cd80896693dff2dd778e3a4c15d9e8723a /kernel/vconv.ml | |
| parent | 326799c4404c08ebf4ae8f8937925d83ac2246b0 (diff) | |
Efficient filtered functions in Evd. We test that a filter is actually
different from the identity before trying to compute filtered env/hyps.
According to profiling, it seems that the filter operation is NEVER taken,
that is, all filters that reach toplevel are dummy. There is surely something
to do here...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16960 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/vconv.ml')
0 files changed, 0 insertions, 0 deletions