diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-05 17:28:56 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-05 17:28:56 +0000 |
| commit | ab7377de0a913ca6218bc7377fab33b8018f8f59 (patch) | |
| tree | 23831c70da9e71cc20a65670e721dc74277fce9c /checker/check.mllib | |
| parent | 0737d090ed32c0857757b76dc94bb5aaa1a096ef (diff) | |
Optimizing some evar_maps manipulation. In particular, using a [map] instead
of a [fold] in [nf_*] normalizing functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16764 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/check.mllib')
0 files changed, 0 insertions, 0 deletions