diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-03-02 10:58:28 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | 0ab98d3380033b58162015656f435ae90b936856 (patch) | |
| tree | 38a17503ccbc5fd51d473f458e782812360ed5b1 /src/Reflection/Named | |
| parent | 7f0ba34481f59db0cf430d7a08b8b65d953eb803 (diff) | |
make 8.5 happy
Diffstat (limited to 'src/Reflection/Named')
| -rw-r--r-- | src/Reflection/Named/Syntax.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v index 996d707a3..1f171e9af 100644 --- a/src/Reflection/Named/Syntax.v +++ b/src/Reflection/Named/Syntax.v @@ -187,7 +187,7 @@ Global Arguments wff {_ _ _ _ _} ctx {t} _. Global Arguments wf {_ _ _ _ _} ctx {t} _. Global Arguments interp_genf {_ _ _ var _} _ _ _ _ _ _ {ctx t} _ _. Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _ _. -Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _. +Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _ _. Notation "'slet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope. Notation "'λn' x .. y , t" := (Abs x .. (Abs y t%nexpr) .. ) : nexpr_scope. |