From bba9f9df9f6064f38f1ac6edfe9d5327bd3abfb6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Sep 2016 11:40:35 -0400 Subject: MxDH: do not depend on implicit import of list notations --- src/Spec/MxDH.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Spec') 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. -- cgit v1.2.3