Debugging stuff removed.

[helm.git] / helm / gTopLevel / proofEngineReduction.ml

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 52f07e4dc2411d8b8aa63a75fcb290c3ebefe044..58aaa04386329ef8e0de0283fa449e84bc0612d2 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -59,7 +59,11 @@ let replace ~what ~with_what ~where =
     | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
     | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
-    | C.Appl l -> C.Appl (List.map aux l)
+    | C.Appl l ->
+       (* Invariant enforced: no application of an application *)
+       (match List.map aux l with
+           (C.Appl l')::tl -> C.Appl (l'@tl)
+         | l' -> C.Appl l')
     | C.Const _ as t -> t
     | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
@@ -242,10 +246,7 @@ let reduce =
        in
         if l = [] then t' else C.Appl (t'::l)
  in
-function t -> let res =
-prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
   reduceaux []
-t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
 ;;
 
 exception WrongShape;;