diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-27 15:37:55 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-27 15:37:55 -0400 |
| commit | d92c5215b802e31022297ab35f7c69936d10dc56 (patch) | |
| tree | 934d539960550ab7da8be334f1f3b11268be063f /src | |
| parent | 6d3772435f9924df0984c8050766b154d7c41f8d (diff) | |
Add Inline import
N.B. The proof of Wf for InlineConst is currently admitted
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Reify.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v index 07c94cee6..44689a2c3 100644 --- a/src/Reflection/Z/Reify.v +++ b/src/Reflection/Z/Reify.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Inline. Require Import Crypto.Reflection.Linearize. Ltac base_reify_op op op_head ::= |