diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-03 17:15:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-04 18:42:47 +0200 |
| commit | a260d05933b8e2c53cb0935442c5b60484fdfc6c (patch) | |
| tree | d6ed6fa3aed4b812525614c67a4c1031342d5c01 /theories/Reals/Rtrigo_calc.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/Rtrigo_calc.v')
0 files changed, 0 insertions, 0 deletions