From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 1 Jul 2002 20:10:54 +0000 (+0000)
Subject: bug fix: handled LetIn case in simpl
X-Git-Tag: V_0_3_0_debian_8~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e94ade9e36f123a555a7727be1e0ae722841426;p=helm.git

bug fix: handled LetIn case in simpl
---

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,_) ->