diff options
| author | ppedrot | 2013-11-08 19:03:52 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-08 19:03:52 +0000 |
| commit | 0a296b7a3fd39f6b2117c0278219a382d2c207c2 (patch) | |
| tree | 5d7bf64ee896806630c65131a2565de39ccf3054 /interp/notation.mli | |
| parent | 6a1564cf51b0fa157a822225d5b7f78dc14b42ad (diff) | |
Useless array manipulation in Rtrees.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17070 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions