aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/R_sqr.v
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-22 19:31:18 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-22 19:34:01 +0100
commit947d93a8b7ff0fc7ba23633fcd44820427e29326 (patch)
tree8257bdccc135ec71108ebfa1fc212951c9271abf /theories/Reals/R_sqr.v
parent8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff)
Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.
This adds at least support for camlp5 6.14 (in addition to 6.17).
Diffstat (limited to 'theories/Reals/R_sqr.v')
0 files changed, 0 insertions, 0 deletions