diff options
Diffstat (limited to 'src/Spec/MxDH.v')
| -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. |