From 58004b95e09ac46115883c4d29d69cfa58184e56 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 Nov 2001 18:32:04 +0000 Subject: [PATCH] LetIn reduction (alias zeta-reduction) is now performed during whd. --- helm/ocaml/cic_proof_checking/cicReduction.ml | 1 + 1 file changed, 1 insertion(+) 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 -> -- 2.39.2