diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 20:47:51 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 20:47:51 -0700 |
| commit | c61e00850385507f75c51c08c7a7bb7e7ab51417 (patch) | |
| tree | b813f87f01f817f670191a2c4e6f18aa6081c0d0 /src | |
| parent | a476968e7cc5b38e9de14837eae23c81ff4b88d7 (diff) | |
Better implicits for interp_type_gen_rel_pointwise
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Syntax.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 6d632342b..89b5eb1f1 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -209,7 +209,9 @@ Global Arguments Let {_ _ _ _ _} _ {_} _. Global Arguments Pair {_ _ _ _ _} _ {_} _. Global Arguments Return {_ _ _ _ _} _. Global Arguments Abs {_ _ _ _ _ _} _. +Global Arguments interp_type_gen {_} _ _. Global Arguments interp_flat_type_gen {_} _ _. +Global Arguments interp_type_gen_rel_pointwise {_} _ _ {_} _ _. Global Arguments interp_type {_} _ _. Global Arguments wff {_ _ _ _ _} G {t} _ _. Global Arguments wf {_ _ _ _ _} G {t} _ _. |