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 0dc4ce4ee3e617a1b1cb6a98efa6dc68db8e922b..1502b600f3c6122b4f37f0918bfe7aeb0e2f2384 100644 (file)
--- 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 5d3be8cb14180a09d7154871a7be831a5d7863a4..e9b144acc76f3f57093c4140decd89daca7ea240 100644 (file)
--- 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;