Allow inlining expressions not returning Tbase

4 files changed, 8 insertions, 5 deletions

diff --git a/src/Compilers/Inline.v b/src/Compilers/Inline.v
index d2aa44520..e4946adde 100644
--- a/src/Compilers/Inline.v
+++ b/src/Compilers/Inline.v
@@ -20,13 +20,13 @@ Section language.
 
     Inductive inline_directive : flat_type -> Type :=
     | default_inline {t} (e : @exprf var t) : inline_directive t
-    | inline {t : base_type_code} (e : @exprf var t) : inline_directive t
+    | inline {t} (e : interp_flat_type (fun t => @exprf var (Tbase t)) t) : inline_directive t
     | no_inline {t} (e : @exprf var t) : inline_directive t.
 
     Definition exprf_of_inline_directive {t} (v : inline_directive t) : @exprf var t
       := match v with
          | default_inline t e => e
-         | inline t e => e
+         | inline t e => SmartPairf e
          | no_inline t e => e
          end.
 
@@ -63,7 +63,7 @@ Section language.
       Definition postprocess_for_const (t : flat_type) (v : @exprf var t) : inline_directive t
         := if match v with Op _ _ op _ => @is_const _ _ op | _ => false end
            then match t return @exprf _ t -> inline_directive t with
-                | Syntax.Tbase _ => @inline _
+                | Syntax.Tbase _ => @inline (Tbase _)
                 | _ => @default_inline _
                 end v
            else default_inline v.
diff --git a/src/Compilers/InlineInterp.v b/src/Compilers/InlineInterp.v
index 397290ef8..caef4245a 100644
--- a/src/Compilers/InlineInterp.v
+++ b/src/Compilers/InlineInterp.v
@@ -61,6 +61,7 @@ Section language.
     | [ H : _, H' : _ |- _ ] => rewrite H in H' by fail
     | [ H : _ |- _ ] => apply H; solve [ repeat t_fin_step ]
     | [ H : _ |- _ ] => rewrite H; solve [ repeat t_fin_step ]
+    | _ => solve [ eapply WfProofs.flatten_binding_list_interpf_SmartPairf_same; eauto ]
     end.
   Local Ltac t_fin := repeat t_fin_step.
 
diff --git a/src/Compilers/InlineWf.v b/src/Compilers/InlineWf.v
index a0d77471c..84bf07fb7 100644
--- a/src/Compilers/InlineWf.v
+++ b/src/Compilers/InlineWf.v
@@ -62,7 +62,8 @@ Section language.
                    | progress subst
                    | solve [ auto with nocore
                            | eapply (@wff_SmartVarVarf _ _ _ _ _ _ (_ * _)); auto
-                           | eapply wff_SmartVarVarf; eauto with nocore ]
+                           | eapply wff_SmartVarVarf; eauto with nocore
+                           | eapply wff_SmartPairf; eauto with nocore ]
                    | progress simpl in *
                    | constructor
                    | solve [ eauto ] ].
@@ -167,6 +168,7 @@ Section language.
                      | progress inversion_prod
                      | progress destruct_head' False
                      | progress simpl in *
+                     | progress unfold SmartMap.SmartPairf
                      | progress invert_expr
                      | progress inversion_wf
                      | progress break_innermost_match_step
diff --git a/src/Specific/NISTP256/FancyMachine256/Core.v b/src/Specific/NISTP256/FancyMachine256/Core.v
index 49d7a2b87..fec353c6f 100644
--- a/src/Specific/NISTP256/FancyMachine256/Core.v
+++ b/src/Specific/NISTP256/FancyMachine256/Core.v
@@ -125,7 +125,7 @@ Section reflection.
        | opt_noinline => no_inline e
        | opt_default => default_inline e
        | opt_inline => match t as t' return exprf _ _ t' -> inline_directive t' with
-                       | Tbase _ => fun e => inline e
+                       | Tbase _ => fun e => @inline _ _ _ (Tbase _) e
                        | _ => fun e => default_inline e
                        end e
        end.