bug fix: handled LetIn case in simpl

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 941a701a920df3b6424fa504efbfecd89e076ab2..8589a64429665b14bdbc4598d24f2bbe092a8b38 100644 (file)
--- 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,_) ->