diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-13 13:05:10 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-13 13:56:29 -0500 |
| commit | 08f5ede8d8466ad9bbf695a8c069d08d4dfc734a (patch) | |
| tree | 14feb03e26dee7f0058a953d96fdedf7d3ba138e /src/Util/DefaultedTypes.v | |
| parent | 011e29790182b3c85889ce402f7fc9fad0ac0817 (diff) | |
Make pipeline options more easily extensible
Also add a dummy option about renaming binders, to be used in an
upcoming commit.
Diffstat (limited to 'src/Util/DefaultedTypes.v')
| -rw-r--r-- | src/Util/DefaultedTypes.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/DefaultedTypes.v b/src/Util/DefaultedTypes.v new file mode 100644 index 000000000..37d9c25ef --- /dev/null +++ b/src/Util/DefaultedTypes.v @@ -0,0 +1,2 @@ +Class with_default (T : Type) (default : T) := defaulted : T. +Global Instance by_default {T} {d} : with_default T d := d. |