Key on the head of the operation in reification

Hopefully fixes #62

Also, don't export InputSyntax in Reify

2 files changed, 6 insertions, 5 deletions

diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v
index 58ebd5da5..d5d2b219e 100644
--- a/src/Reflection/Reify.v
+++ b/src/Reflection/Reify.v
@@ -3,7 +3,7 @@
     judgmental equality of the denotation of the reified term. *)
 Require Import Coq.Strings.String.
 Require Import Crypto.Reflection.Syntax.
-Require Export Crypto.Reflection.InputSyntax.
+Require Import Crypto.Reflection.InputSyntax.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
@@ -134,7 +134,8 @@ Ltac reifyf base_type_code interp_base_type op var e :=
     let t := lazymatch type of x with ?t => reify_type t end in
     let retv := match constr:(Set) with
                 | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv)
-                | _ => let r := constr:(_ : reify_op op x _ _) in
+                | _ => let op_head := head x in
+                       let r := constr:(_ : reify_op op op_head _ _) in
                        let t := type of r in
                        constr:(op_info t)
                 | _ => let c := mkConst t x in
diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v
index 17580aa5d..457c9fcfe 100644
--- a/src/Reflection/TestCase.v
+++ b/src/Reflection/TestCase.v
@@ -26,9 +26,9 @@ Definition interp_op src dst (f : op src dst) : interp_flat_type_gen interp_base
      | Sub => fun xy => fst xy - snd xy
      end%nat.
 
-Global Instance: forall x y, reify_op op (x + y)%nat 2 Add := fun _ _ => I.
-Global Instance: forall x y, reify_op op (x * y)%nat 2 Mul := fun _ _ => I.
-Global Instance: forall x y, reify_op op (x - y)%nat 2 Sub := fun _ _ => I.
+Global Instance: reify_op op plus 2 Add := I.
+Global Instance: reify_op op mult 2 Mul := I.
+Global Instance: reify_op op minus 2 Sub := I.
 Global Instance: reify type nat := Tnat.
 
 Ltac Reify' e := Reify.Reify' base_type interp_base_type op e.