From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 Sep 2005 15:25:56 +0000 (+0000)
Subject: fix generation of applications of applications.
X-Git-Tag: V_0_1_2_1~99
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3314de1ff7affc9c82b8b4b63453a36ce2bcf64;p=helm.git

fix generation of applications of applications.
---

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 087d32775..cced961c0 100644
--- 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)