diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-16 16:17:37 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-16 16:17:37 -0500 |
| commit | c5d0ab81dc81a7fdcb3d681bd319afa9a5789800 (patch) | |
| tree | 84f46ba4dac91149b8eb6a9934f605d6de169480 /src/Specific | |
| 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/Specific')
| -rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 65c7d92b8..76cf82bd1 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/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) f k)). + (fun k => UnReturn (Apply length_fe25519 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) - (Apply (n:=length_fe25519) + => UnReturn (Apply length_fe25519 + (Apply length_fe25519 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) f k)). + (fun k => UnReturn (Apply length_fe25519 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) f k)). + (fun k => UnReturn (Apply length_fe25519 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the |