Fix 8.4 build partially

2 files changed, 4 insertions, 4 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 197a0dca6..3b0231191 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -532,7 +532,7 @@ Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B int_width :=
    c_reduce1 : c * ((2 ^ B) >> nth_default 0 limb_widths (pred (length limb_widths))) <= 2 ^ (nth_default 0 limb_widths 0);
    (* on the second reduce step, we add at most one bit of width to the first digit,
       and leave room to carry c one more time after the highest bit is carried *)
-   c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c;
+   c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c
   }.
 
 Section CanonicalizationProofs.
diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v
index 8e70648fd..2f0b19faa 100644
--- a/src/Reflection/Z/Interpretations.v
+++ b/src/Reflection/Z/Interpretations.v
@@ -637,21 +637,21 @@ Module Relations.
                {t : type base_type}
       : interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop
       := match t return interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop  with
-         | Tflat T => R
+         | Tflat T => @R _
          | Arrow A B
            => fun f g
               => forall x : interp_flat_type (fun _ => interp_base_type1) (all_binders_for (Arrow A B)),
                   let y := SmartVarfMap proj_option x in
                   let fx := ApplyInterpedAll f (LiftOption.to' (Some x)) in
                   let gy := ApplyInterpedAll g y in
-                  R fx gy
+                  @R _ fx gy
          end.
 
     Lemma uncurry_interp_type_rel_pointwise2_proj_option
           {t : type base_type}
           {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t}
           {g}
-    : interp_type_rel_pointwise2 (t:=t) (fun t => R) f g
+    : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g
       -> interp_type_rel_pointwise2_uncurried_proj_option (t:=t) f g.
     Proof.
       unfold interp_type_rel_pointwise2_uncurried_proj_option.