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