aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Saturated/Freeze.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Arithmetic/Saturated/Freeze.v')
-rw-r--r--src/Arithmetic/Saturated/Freeze.v6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Arithmetic/Saturated/Freeze.v b/src/Arithmetic/Saturated/Freeze.v
index 735663636..65b8ee55d 100644
--- a/src/Arithmetic/Saturated/Freeze.v
+++ b/src/Arithmetic/Saturated/Freeze.v
@@ -119,4 +119,8 @@ Section Freeze.
rewrite Z.add_0_r, Z.mod_mod by assumption.
reflexivity. }
Qed.
-End Freeze. \ No newline at end of file
+End Freeze.
+
+Hint Unfold
+ freeze freeze_cps
+ : basesystem_partial_evaluation_unfolder.