diff options
Diffstat (limited to 'src/Specific/GF1305.v')
| -rw-r--r-- | src/Specific/GF1305.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index edb122ac2..057676ee2 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -48,11 +48,11 @@ Definition fe1305 : Type := Eval cbv in fe. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In. -Definition mul (f g:fe1305) : { fg | fg = ModularBaseSystemInterface.mul k_subst c_subst f g }. +Definition mul (f g:fe1305) : { fg | fg = @ModularBaseSystemInterface.mul _ _ k_ c_ f g }. (* NOTE: beautiful example of reduction slowness: stack overflow if [f] [g] are not destructed first *) cbv [fe1305] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - eexists. + eexists. cbv. autorewrite with zsimplify. reflexivity. |