aboutsummaryrefslogtreecommitdiff
path: root/theories/Program/Wf.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program/Wf.v')
-rw-r--r--theories/Program/Wf.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 688db8b812..d1be8812e9 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -108,6 +108,7 @@ Section Measure_well_founded.
End Measure_well_founded.
+#[global]
Hint Resolve measure_wf : core.
Section Fix_rects.