aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rtrigo_def.v
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-28 17:30:02 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-28 20:58:24 +0200
commit2a45c6df8b243ddd3e70e8b5244d1ce8014e7970 (patch)
tree48749808f695651cc7d21b313535cf34e4126cf1 /theories/Reals/Rtrigo_def.v
parentca427f04ca477895117d16a78eefd1ed4ad1876f (diff)
Patterns: Accepting patterns in PFix and PCofix and not only constr.
Diffstat (limited to 'theories/Reals/Rtrigo_def.v')
0 files changed, 0 insertions, 0 deletions