diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-09-27 16:15:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-09-27 16:15:22 -0400 |
| commit | 63da3166914ea3c7de954f1015fea3df305bf5b6 (patch) | |
| tree | 5e8ca16b6c26e25887c740357375384961e18fbf /src | |
| parent | bdcc7c30e374eb3aebb6de30c3fbf9e4555194c6 (diff) | |
Add missing tactic in comment in ladderstep
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/X25519/C64/ladderstep.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v index adafa6d56..9e2187a81 100644 --- a/src/Specific/X25519/C64/ladderstep.v +++ b/src/Specific/X25519/C64/ladderstep.v @@ -158,6 +158,7 @@ Section BoundedField25p5. { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } + { Time abstract ReflectiveTactics.handle_boundedness_side_condition. } *) Time refine_reflectively. Show Ltac Profile. |