Add support for dependent reification

3 files changed, 6 insertions, 6 deletions

diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v
index ed9646eb4..1a2f22eca 100644
--- a/src/Reflection/Reify.v
+++ b/src/Reflection/Reify.v
@@ -68,11 +68,11 @@ Inductive reify_result_helper :=
 | reification_unsuccessful.
 
 (** Override this to get a faster [reify_op] *)
-Ltac base_reify_op op op_head :=
+Ltac base_reify_op op op_head expr :=
   let r := constr:(_ : reify_op op op_head _ _) in
   type of r.
-Ltac reify_op op op_head :=
-  let t := base_reify_op op op_head in
+Ltac reify_op op op_head expr :=
+  let t := base_reify_op op op_head expr in
   constr:(op_info t).
 
 (** Change this with [Ltac reify_debug_level ::= constr:(1).] to get
@@ -152,7 +152,7 @@ Ltac reifyf base_type_code interp_base_type op var e :=
     let retv := match constr:(Set) with
                 | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv)
                 | _ => let op_head := head x in
-                       reify_op op op_head
+                       reify_op op op_head x
                 | _ => let c := mkConst t x in
                        constr:(finished_value c)
                 | _ => constr:(reification_unsuccessful)
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v
index 3c42c162c..451e522d0 100644
--- a/src/Reflection/Z/Reify.v
+++ b/src/Reflection/Z/Reify.v
@@ -9,7 +9,7 @@ Require Import Crypto.Reflection.InlineInterp.
 Require Import Crypto.Reflection.Linearize.
 Require Import Crypto.Reflection.LinearizeInterp.
 
-Ltac base_reify_op op op_head ::=
+Ltac base_reify_op op op_head extra ::=
      lazymatch op_head with
      | @Z.add => constr:(reify_op op op_head 2 Add)
      | @Z.mul => constr:(reify_op op op_head 2 Mul)
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index 207237db7..eb443a8e3 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -125,7 +125,7 @@ Section reflection.
   Definition Inline {t} e := @InlineConstGen base_type interp_base_type op postprocess t e.
 End reflection.
 
-Ltac base_reify_op op op_head ::=
+Ltac base_reify_op op op_head expr ::=
      lazymatch op_head with
      | @Interface.ldi => constr:(reify_op op op_head 1 OPldi)
      | @Interface.shrd => constr:(reify_op op op_head 3 OPshrd)