From 10e16fe0fd01f7503fc87bdbbed474bf55e5c2b6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 27 Feb 2016 01:35:37 +0100
Subject: [PATCH] Fallthrough instance for heap lang substitution.

Now we substitute as far into the term as we can. This is to deal
with terms that contain Coq variables.
---
 heap_lang/substitution.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index dcdae63c1..16a865011 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -13,15 +13,16 @@ Hint Mode Subst + + + - : typeclass_instances.
 
 Ltac simpl_subst :=
   repeat match goal with
-  | |- context [subst ?e ?x ?v] => rewrite (@do_subst e x v)
+  | |- context [subst ?e ?x ?v] => progress rewrite (@do_subst e x v)
   | |- _ => progress csimpl
   end; fold of_val.
 
 Arguments of_val : simpl never.
-Hint Extern 10 (Subst (of_val _) _ _ _) =>
-  unfold of_val; fold of_val : typeclass_instances.
-Hint Extern 10 (Closed (of_val _)) =>
-  unfold of_val; fold of_val : typeclass_instances.
+Hint Extern 10 (Subst (of_val _) _ _ _) => unfold of_val : typeclass_instances.
+Hint Extern 10 (Closed (of_val _)) => unfold of_val : typeclass_instances.
+
+Instance subst_fallthrough e x v : Subst e x v (subst e x v) | 1000.
+Proof. done. Qed.
 
 Class SubstIf (P : Prop) (e : expr) (x : string) (v : val) (er : expr) := {
   subst_if_true : P → subst e x v = er;
-- 
GitLab