diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 20:17:03 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 20:17:03 -0700 |
| commit | c7e14293503029ad8df45f495947d5b5e3c91a8a (patch) | |
| tree | 9765c47dcbf971a76e94483257962bf7eafc279a /src | |
| parent | 0f9283bbca9acac6f927ba1dd47806b57e95f89e (diff) | |
Better implicits for interpf
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Syntax.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 71d7e49f1..cc816f58f 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -207,6 +207,7 @@ Global Arguments wf {_ _ _ _ _} G {t} _ _. Global Arguments Wf {_ _ _ t} _. Global Arguments Interp {_ _ _} interp_op {t} _. Global Arguments interp {_ _ _} interp_op {t} _. +Global Arguments interpf {_ _ _} interp_op {t} _. Notation "'slet' x := A 'in' b" := (Let A (fun x => b)) : expr_scope. Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. |