diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-26 11:40:35 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-26 11:40:35 -0400 |
| commit | bba9f9df9f6064f38f1ac6edfe9d5327bd3abfb6 (patch) | |
| tree | e9338ffda4cf5a939b24706ee097b71a4f1f66ac /src/Spec | |
| parent | 4df54112680e25dc797569317862f5abbf941b28 (diff) | |
MxDH: do not depend on implicit import of list notations
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/MxDH.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Spec/MxDH.v b/src/Spec/MxDH.v index 512930fbc..d637836e4 100644 --- a/src/Spec/MxDH.v +++ b/src/Spec/MxDH.v @@ -48,7 +48,7 @@ Module MxDH. (* from RFC7748 *) Fixpoint downto_iter (i:nat) : list nat := match i with - | Datatypes.S i' => i'::downto_iter i' + | Datatypes.S i' => cons i' (downto_iter i') | O => nil end. |