diff options
| author | Emilio Jesus Gallego Arias | 2017-04-25 18:36:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-25 18:43:03 +0200 |
| commit | e699313c7a3829016c853b2a1541c2e9151d709c (patch) | |
| tree | 107f752561421e85cd91e23977f3185e2dea1426 /kernel/nativevalues.ml | |
| parent | 4abb41d008fc754f21916dcac9cce49f2d04dd6d (diff) | |
[toplevel] Remove unused parameter from `Vernac.process_expr`.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions