diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-07 18:49:41 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-07 18:49:41 -0500 |
| commit | e2b043571b6af3f2e25bfebc230e89055ece2745 (patch) | |
| tree | 915c50a2280eedbd306101246aea7b959c44bef1 /src/Specific | |
| parent | 7a7a62468fdfe3d12ecc75b01e502af03daa1f3b (diff) | |
Clean up and improve Reflection.Relations
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 900a9f50c..968f83be9 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -509,7 +509,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := repeat match goal with x := _ |- _ => subst x end; cbv [id binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded - Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; + Relations.proj_eq_rel interp_flat_type_rel_pointwise SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; lazymatch goal with | [ |- fe25519WToZ ?x = _ /\ _ ] => generalize dependent x; intros |