We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 1023dda commit adb436aCopy full SHA for adb436a
test-suite/bugs/bug_5198.v
@@ -29,7 +29,7 @@ Definition SRepAdd : forall (_ _ : SRep), SRep
29
:= let v := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)) in
30
v.
31
Definition SRepAdd' : forall (_ _ : SRep), SRep
32
- := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)).
+ := (fun x y => barrett_reduce_function_bundled (@CarryAdd (f (S O) O) _ x y)).
33
(* Error:
34
In environment
35
x : SRep
0 commit comments