fix generation of applications of applications.

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 087d327757babbe020e167c8babd40821bdaf3b5..cced961c0fa54b838d25940805971554818d5540 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -601,6 +601,14 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
+ let mk_appl t l =
+   if l = [] then 
+     t 
+   else 
+     match t with
+     | Cic.Appl l' -> Cic.Appl (l'@l)
+     | _ -> Cic.Appl (t::l)
+ in
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
@@ -614,8 +622,7 @@ let simpl context =
             Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
           | Some (_,C.Def (bo,_)) ->
              let lifted_bo = S.lift n bo in
-             let applied_lifted_bo =
-              if l = [] then lifted_bo else C.Appl (lifted_bo::l) in
+             let applied_lifted_bo = mk_appl lifted_bo l in
              let simplified = try_delta_expansion context l t lifted_bo in
               if simplified = applied_lifted_bo then
                if l = [] then t else C.Appl (t::l)