More 8.4 fixes

3 files changed, 3 insertions, 2 deletions

diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v
index 1d21b18ae..781643a8a 100644
--- a/src/Reflection/InlineWf.v
+++ b/src/Reflection/InlineWf.v
@@ -65,6 +65,7 @@ Section language.
       | [ H : _ |- _ ]
         => pose proof (IHwf _ H) as IHwf'
       end.
+      generalize dependent (inline_constf e1); generalize dependent (inline_constf e1'); intros.
       destruct IHwf'; simpl in *;
         repeat constructor; auto; intros;
           match goal with
diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v
index 618523e55..d68ed53ac 100644
--- a/src/Reflection/WfReflective.v
+++ b/src/Reflection/WfReflective.v
@@ -233,7 +233,7 @@ Section Wf.
     intros H var1 var2; specialize (H var1 var2).
     pose proof (@reflect_wf base_type_code interp_base_type base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 nil t t (e _) (e _)) as H'.
     rewrite type_eq_semidec_transparent_refl in H' by assumption; simpl in *.
-    edestruct reflect_wfT; simpl in *; tauto.
+    edestruct @reflect_wfT; simpl in *; tauto.
   Qed.
 
   (** Leads to larger proofs (an extra constant factor which is the
diff --git a/src/Reflection/WfRelReflective.v b/src/Reflection/WfRelReflective.v
index f2af49ccf..0135f6afb 100644
--- a/src/Reflection/WfRelReflective.v
+++ b/src/Reflection/WfRelReflective.v
@@ -63,7 +63,7 @@ Section language.
            end.
   Local Ltac t_step :=
     match goal with
-    | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, preflatten_binding_list2, option_map, and_option_pointed_Prop, eq_semidec_and_gen in *
+    | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, WfReflectiveGen.preflatten_binding_list2, option_map, and_option_pointed_Prop, eq_semidec_and_gen in *
     | _ => progress simpl in *
     | _ => progress break_match
     | _ => progress subst