diff options
author | 2014-06-03 17:15:40 +0200 | |
---|---|---|
committer | 2014-06-04 18:42:47 +0200 | |
commit | a260d05933b8e2c53cb0935442c5b60484fdfc6c (patch) | |
tree | d6ed6fa3aed4b812525614c67a4c1031342d5c01 /theories/Reals/RList.v | |
parent | e1e0f4f7f3c549fd3d5677b67c6b13ed687e6f12 (diff) |
Make standard library independent of the names generated by
induction/elim over a dependent elimination principle for Prop
arguments.
Diffstat (limited to 'theories/Reals/RList.v')
0 files changed, 0 insertions, 0 deletions