diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-07 11:50:23 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-07 11:50:23 -0700 |
| commit | e4e860f8b10a1b8ce1ab207f12c7ef50e36332c4 (patch) | |
| tree | a23a96bcb0b69e04d976ea60b287c5dd434efc47 /src/Reflection/Reify.v | |
| parent | e233e15c0eafd34d9cb6412361d7aaa373d774e0 (diff) | |
Key on the head of the operation in reification
Hopefully fixes #62
Also, don't export InputSyntax in Reify
Diffstat (limited to 'src/Reflection/Reify.v')
| -rw-r--r-- | src/Reflection/Reify.v | 5 |
1 files changed, 3 insertions, 2 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 |