Reduction tres significative du terme preuve

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1811 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 16 insertions, 12 deletions

diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 4b676e8bb..9a1a1b057 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -147,8 +147,9 @@ Tactic Definition ApplyAssoc FT lvar trm :=
   Cut (interp_ExprA FT lvar (assoc trm))==(interp_ExprA FT lvar trm);
   [Intro;
    (Match Context With
-    | [id:(interp_ExprA ? ? (assoc ?))== ? |- ?] ->
-      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+    | [id:(interp_ExprA ?1 ?2 (assoc ?3))== ?4 |- ?] ->
+      Let t=Eval Compute in (assoc ?3) In
+      Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id)
   |Apply assoc_correct].
 
 (**** Distribution *****)
@@ -157,8 +158,9 @@ Tactic Definition ApplyDistrib FT lvar trm :=
   Cut (interp_ExprA FT lvar (distrib trm))==(interp_ExprA FT lvar trm);
   [Intro;
    (Match Context With
-    | [id:(interp_ExprA ? ? (distrib ?))== ? |- ?] ->
-      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+    | [id:(interp_ExprA ?1 ?2 (distrib ?3))== ?4 |- ?] ->
+      Let t=Eval Compute in (distrib ?3) In
+      Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id)
   |Apply distrib_correct].
 
 (**** Multiplication by the inverse product ****)
@@ -174,8 +176,8 @@ Tactic Definition Multiply mul :=
     Cut ~(interp_ExprA ?1 ?2 mul)==AzeroT;
     [Intro;
      Let id = GrepMult In
-     Apply (mult_eq ?1 ?3 ?4 mul ?2 id);
-     Cbv Beta Delta -[interp_ExprA] Iota
+     Apply (mult_eq ?1 ?3 ?4 mul ?2 id)(*;
+     Cbv Beta Delta -[interp_ExprA] Iota*)
     |Cbv Beta Delta -[not] Iota;
      Let AmultT = Eval Compute in (Amult ?1)
      And AoneT = Eval Compute in (Aone ?1) In
@@ -186,8 +188,9 @@ Tactic Definition ApplyMultiply FT lvar trm :=
   Cut (interp_ExprA FT lvar (multiply trm))==(interp_ExprA FT lvar trm);
   [Intro;
    (Match Context With
-    | [id:(interp_ExprA ? ? (multiply ?))== ? |- ?] ->
-      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+    | [id:(interp_ExprA ?1 ?2 (multiply ?3))== ?4 |- ?] ->
+      Let t=Eval Compute in (multiply ?3) In
+      Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id)
   |Apply multiply_correct].
 
 (**** Permutations and simplification ****)
@@ -197,8 +200,9 @@ Tactic Definition ApplyInverse mul FT lvar trm :=
       (interp_ExprA FT lvar trm);
   [Intro;
    (Match Context With
-   | [id:(interp_ExprA ? ? (inverse_simplif ? ?))== ? |- ?] ->
-     Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+   | [id:(interp_ExprA ?1 ?2 (inverse_simplif ?3 ?4))== ?5 |- ?] ->
+     Let t=Eval Compute in (inverse_simplif ?3 ?4) In
+      Change (interp_ExprA ?1 ?2 t)== ?5 in id;Try (Rewrite <- id);Clear id)
   |Apply inverse_correct;Assumption].
 
 (**** Inverse test ****)
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 2cd2f09a6..5cdd5eacd 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -194,8 +194,8 @@ Save.
 
 Fixpoint interp_ExprA [lvar:(list (Sprod AT nat));e:ExprA] : AT :=
   Cases e of
-  | EAzero            => AzeroT
-  | EAone            => AoneT
+  | EAzero         => AzeroT
+  | EAone          => AoneT
   | (EAplus e1 e2) => (AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2))
   | (EAmult e1 e2) => (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2))
   | (EAopp e)      => ((Aopp T) (interp_ExprA lvar e))