diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 15:46:28 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 15:46:28 -0700 |
| commit | 3beb3fc256e9e34c46275cd005ff0b560e917c9b (patch) | |
| tree | a8f80f191622337a08cb631890d07a08b30a1b93 | |
| parent | 16737faa337e3a47bb2d7283cb57ee93342a3eb0 (diff) | |
Better implicit arguments for linearize
| -rw-r--r-- | src/Reflection/Linearize.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v index b3ce3249b..d7d1fc2b6 100644 --- a/src/Reflection/Linearize.v +++ b/src/Reflection/Linearize.v @@ -97,5 +97,9 @@ Section language. := fun var => inline_const (e _). End language. -Arguments Linearize {_ _ _ _} _ var. -Arguments InlineConst {_ _ _ _} _ var. +Global Arguments linearizef {_ _ _ _ _} _. +Global Arguments linearize {_ _ _ _ _} _. +Global Arguments Linearize {_ _ _ _} _ var. +Global Arguments inline_constf {_ _ _ _ _} _. +Global Arguments inline_const {_ _ _ _ _} _. +Global Arguments InlineConst {_ _ _ _} _ var. |