diff options
author | 2016-11-16 16:17:37 -0500 | |
---|---|---|
committer | 2016-11-16 16:17:37 -0500 | |
commit | c5d0ab81dc81a7fdcb3d681bd319afa9a5789800 (patch) | |
tree | 84f46ba4dac91149b8eb6a9934f605d6de169480 /src/SpecificGen/GF25519_32Reflective/Common.v | |
parent | 091d90cd6b3a8749c3afc7b3e4243841ba5e25d8 (diff) |
Work around bug #5205 (arguments naming weirdness)
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5205, Bogus "Error:
Wrong argument name: n." error message in 8.4, 8.5
Diffstat (limited to 'src/SpecificGen/GF25519_32Reflective/Common.v')
-rw-r--r-- | src/SpecificGen/GF25519_32Reflective/Common.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v index b1eb33329..5df38d38d 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common.v +++ b/src/SpecificGen/GF25519_32Reflective/Common.v @@ -344,28 +344,28 @@ Defined. Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var := fun x => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply (n:=length_fe25519_32) f k)). + (fun k => UnReturn (Apply length_fe25519_32 f k)). Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var := fun x y => LetIn (UnReturn (unop_make_args x)) (fun x' => LetIn (UnReturn (unop_make_args y)) (fun y' - => UnReturn (Apply (n:=length_fe25519_32) - (Apply (n:=length_fe25519_32) + => UnReturn (Apply length_fe25519_32 + (Apply length_fe25519_32 f x') y'))). Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var := fun x => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply (n:=length_fe25519_32) f k)). + (fun k => UnReturn (Apply length_fe25519_32 f k)). Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var := fun x => LetIn (UnReturn (unop_wire_make_args x)) - (fun k => UnReturn (Apply (n:=List.length wire_widths) f k)). + (fun k => UnReturn (Apply (List.length wire_widths) f k)). Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var := fun x => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply (n:=length_fe25519_32) f k)). + (fun k => UnReturn (Apply length_fe25519_32 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the |