From 7e94ade9e36f123a555a7727be1e0ae722841426 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 1 Jul 2002 20:10:54 +0000 Subject: [PATCH] bug fix: handled LetIn case in simpl --- helm/gTopLevel/proofEngineReduction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 941a701a9..8589a6442 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -331,7 +331,6 @@ let reduce context = exception WrongShape;; exception AlreadySimplified;; -exception WhatShouldIDo;; (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *) (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *) @@ -420,7 +419,8 @@ let simpl context = (* superfluous *) aux (he::rev_constant_args) tl (S.subst he t) end - | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *) + | C.LetIn (_,s,t) -> + aux rev_constant_args l (S.subst s t) | C.Fix (i,fl) as t -> let tys = List.map (function (name,_,ty,_) -> -- 2.39.2