From 0af8d2b4324d57443b1187737d946c70a2acf5a0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Feb 2016 10:31:49 +0100
Subject: [PATCH] dome more doc for gsubst

---
 heap_lang/substitution.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 2d8ce873f..27d57f967 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -12,6 +12,10 @@ unfolding any Coq definitions. For example:
 >>
 
 For [gsubst e x ev] to work, [e] should not contain any opaque parts.
+Fundamentally, the way this works is that [gsubst] tests whether a subterm
+needs substitution, before it traverses into the term. This way, unaffected
+sub-terms are returned directly, rather than their tree structure being
+deconstructed and composed again.
 
 The function [gsubst e x ev] differs in yet another way from [subst e x v].
 The function [gsubst] substitutes an expression [ev] whereas [subst]
-- 
GitLab