From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 Nov 2001 18:32:04 +0000 (+0000)
Subject: LetIn reduction (alias zeta-reduction) is now performed during whd.
X-Git-Tag: mlminidom_0_2_2~45
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=58004b95e09ac46115883c4d29d69cfa58184e56;p=helm.git

LetIn reduction (alias zeta-reduction) is now performed during whd.
---

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 285e660a8..a6f6ee23b 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -86,6 +86,7 @@ let whd =
          | he::tl -> whdaux tl (S.subst he t)
            (* when name is Anonimous the substitution should be superfluous *)
        )
+    | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t)
     | C.Appl (he::tl) -> whdaux (tl@l) he
     | C.Appl [] -> raise (Impossible 1)
     | C.Const (uri,cookingsno) as t ->