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 285e660a8fce5dcdc26ab14c8bdc587b525f4ecf..a6f6ee23b8e638452caf4a681ca1c6bf96585e96 100644 (file)
--- 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 ->