Fix for 8.4's type inferencer being broken

1 files changed, 17 insertions, 6 deletions

diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v
index 2a3d193ac..9cf82b3e2 100644
--- a/src/Reflection/LinearizeWf.v
+++ b/src/Reflection/LinearizeWf.v
@@ -126,10 +126,21 @@ Section language.
                             | Let _ ex _ eC => wff_under_letsf G _ ex
                             | _ => I
                             end);
-          generalize (fun G => match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
-                            | Let _ ex _ eC => fun x => wff_under_letsf G _ (eC x)
-                            | _ => I
-                            end);
+          generalize (fun G => match e1v return match e1v with
+                                                | Let tx0 _ tC1 e0 => (* 8.4's type inferencer is broken, so we copy/paste the term from 8.5.  This entire clause could just be [_], if Coq 8.4 worked *)
+                                                  forall (x : @interp_flat_type_gen base_type_code var1 tx0) (e3 : exprf tC1)
+                                                         (tC2 : flat_type) (eC3 : @interp_flat_type_gen base_type_code var1 tC1 -> exprf tC2)
+                                                         (eC4 : @interp_flat_type_gen base_type_code var2 tC1 -> exprf tC2),
+                                                    wff G (e0 x) e3 ->
+                                                    (forall (x1 : @interp_flat_type_gen base_type_code var1 tC1)
+                                                            (x2 : @interp_flat_type_gen base_type_code var2 tC1),
+                                                        wff (@flatten_binding_list base_type_code var1 var2 tC1 x1 x2 ++ G) (eC3 x1) (eC4 x2)) ->
+                                                    wff G (@under_letsf base_type_code interp_base_type op var1 tC1 (e0 x) tC2 eC3)
+                                                        (@under_letsf base_type_code interp_base_type op var2 tC1 e3 tC2 eC4)
+                                                | _ => _ end with
+                               | Let _ ex tC' eC => fun x => wff_under_letsf G tC' (eC x)
+                               | _ => I
+                               end);
           clear wff_under_letsf
         | generalize (fun G => match e1v return match e1v with Pair _ _ _ _ => _ | _ => _ end with
                             | Pair _ ex _ ey => wff_under_letsf G _ ex
@@ -221,7 +232,7 @@ Section language.
              {struct e1}
       : @wff var1 var2 G t (inline_constf e1) (inline_constf e2).
     Proof.
-      revert H.
+      (*revert H.
       set (e1v := e1) in *.
       destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ];
         [ clear wff_inline_constf
@@ -268,7 +279,7 @@ Section language.
       4:t_fin idtac.
       { match goal with
         | [ H : _ |- _ ] => eapply H; [ | solve [ eauto ] ]; t_fin idtac
-        end. }
+        end. }*)
     Abort.
   End with_var.