diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-15 12:29:27 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-15 12:29:27 -0500 |
| commit | a2cf2ba8acf49238e704bad31d2e2aa7f336c7dd (patch) | |
| tree | 03c07e035164e5926b0ad4deb91608f0dfc59f24 /src/Specific | |
| parent | 3f15fbb04befe1c6d726c33e425d303bf2315dc3 (diff) | |
Fix for Coq 8.5 (more unfolding)
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 324113101..5ee903658 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -350,7 +350,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := cbv [id binop_args_to_bounded unop_args_to_bounded unopWireToFE_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.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; - match goal with + lazymatch goal with | [ |- fe25519WToZ ?x = _ /\ _ ] => generalize dependent x; intros | [ |- wire_digitsWToZ ?x = _ /\ _ ] @@ -358,7 +358,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := | [ |- _ = _ ] => exact Hbounds_left end; - cbv [interp_flat_type WordW.interp_base_type remove_all_binders] in *; + cbv [interp_type interp_type_gen interp_type_gen_hetero interp_flat_type WordW.interp_base_type remove_all_binders] in *; destruct_head' prod; change word64ToZ with WordW.wordWToZ in *; (split; [ exact Hbounds_left | ]); |