Fix for Coq 8.5 (more unfolding)

7 files changed, 14 insertions, 14 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 | ]);
diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index 0414d2188..1f9ec0b9f 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/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
   | [ |- fe2213_32WToZ ?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 | ]);
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index d2e349bd6..dc6c8e12b 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/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
   | [ |- fe2519_32WToZ ?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 | ]);
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index f1b476717..8ee8f5d67 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/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
   | [ |- fe25519_32WToZ ?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 | ]);
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index 3056569bd..f407a51c8 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/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
   | [ |- fe25519_64WToZ ?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 word128ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index dcf396580..8ef1b131b 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/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
   | [ |- fe41417_32WToZ ?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 | ]);
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index 69382ec40..114b930f8 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/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
   | [ |- fe5211_32WToZ ?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 | ]);