diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-28 17:30:02 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-28 20:58:24 +0200 |
commit | 2a45c6df8b243ddd3e70e8b5244d1ce8014e7970 (patch) | |
tree | 48749808f695651cc7d21b313535cf34e4126cf1 /theories/Reals/Rtrigo_def.v | |
parent | ca427f04ca477895117d16a78eefd1ed4ad1876f (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