X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=87cf24c2158be45bf601d879c4bfc2690315ec84;hb=4020414d9bc31b545e311760045d4ce8f0645916;hp=941a701a920df3b6424fa504efbfecd89e076ab2;hpb=7e60b896247a228beea1b2a547c1f606e1834921;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 941a701a9..87cf24c21 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2002, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -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,_) ->