aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Reflection/Z/Reify.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v
index 44689a2c3..4fcb16638 100644
--- a/src/Reflection/Z/Reify.v
+++ b/src/Reflection/Z/Reify.v
@@ -22,7 +22,7 @@ Ltac base_reify_type T ::=
lazymatch T with
| Z => TZ
end.
-Ltac Reify' e := Reify.Reify' base_type interp_base_type op e.
+Ltac Reify' e := Reflection.Reify.Reify' base_type interp_base_type op e.
Ltac Reify e :=
- let v := Reify.Reify base_type interp_base_type op e in
+ let v := Reflection.Reify.Reify base_type interp_base_type op e in
constr:((*Inline _*) ((*CSE _*) ((*InlineConst*) (Linearize v)))).