From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Feb 2006 21:17:16 +0000 (+0000)
Subject: Bug fixed in simplify: delta expansion of constants applied to more arguments
X-Git-Tag: 0.4.95@7852~1636
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0f06e39d49460377dfa214b3d471b71cb9111f48;p=helm.git

Bug fixed in simplify: delta expansion of constants applied to more arguments
than head lambda abstractions was always performed (even if no "interesting"
reduction took place).
---

diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml
index 0dc4ce4ee..1502b600f 100644
--- a/components/tactics/proofEngineReduction.ml
+++ b/components/tactics/proofEngineReduction.ml
@@ -859,10 +859,11 @@ let simpl context =
          | C.LetIn (_,s,t) -> aux l (S.subst s t)
          | t ->
             let simplified = reduceaux context l t in
-            if t = simplified then
-             raise AlreadySimplified
-            else
-             simplified
+            let t' = if l = [] then t else C.Appl (t::l) in
+             if t' = simplified then
+              raise AlreadySimplified
+             else
+              simplified
        in
         (try aux l body
          with
diff --git a/matita/library/algebra/groups.ma b/matita/library/algebra/groups.ma
index 5d3be8cb1..e9b144acc 100644
--- a/matita/library/algebra/groups.ma
+++ b/matita/library/algebra/groups.ma
@@ -243,14 +243,8 @@ theorem member_of_subgroup_op_inv_x_y_to_left_coset_eq:
  ∀G.∀x,y.∀H:subgroup G. (x \sup -1 ·y) ∈ H → x*H = y*H.
 intros;
 unfold left_coset_eq;
-simplify in ⊢ (? → ? ? ? (? ? % ?));
-simplify in ⊢ (? → ? ? ? (? ? ? (? ? ? (? ? %) ?)));
-simplify in ⊢ (? ? % → ?);
-intros;
-unfold member_of_left_coset;
-simplify in ⊢ (? ? (λy:?.? ? ? (? ? ? (? ? ? (? ? %) ?))));
-simplify in ⊢ (? ? (λy:? ? %.?));
-simplify in ⊢ (? ? (λy:?.? ? ? (? ? % ?)));
+simplify;
+intro;
 unfold member_of_subgroup in H1;
 elim H1;
 clear H1;