From 86002ce6e6fb3cbf1f5c9bf3657c13b4e79be192 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 20 Sep 2010 21:59:57 +0000
Subject: Added eta-expansion in kernel, type inference and tactic unification,
 governed in the latter case by a flag since (useful e.g. for setoid rewriting
 which otherwise loops as it is implemented).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/InitialRing.v |  4 +---
 plugins/setoid_ring/Ring_theory.v | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index dcc0c4e410..67bb930921 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -307,9 +307,7 @@ Section NMORPHISM.
   Notation "x == y" := (req x y).
    Add Morphism radd : radd_ext4.  exact (Radd_ext Reqe). Qed.
    Add Morphism rmul : rmul_ext4.  exact (Rmul_ext Reqe). Qed.
-   Add Morphism ropp : ropp_ext4.  exact (Ropp_ext Reqe). Qed.
-   Add Morphism rsub : rsub_ext5.  exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite Rsth Reqe ARth.
+   Ltac norm := gen_srewrite_sr Rsth Reqe ARth.
 
  Definition gen_phiN1 x :=
   match x with
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 581cf9251b..b9f964857d 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -590,6 +590,21 @@ Ltac gen_srewrite Rsth Reqe ARth :=
      | progress rewrite <- (ARopp_mul_l ARth)
      | progress rewrite <- (ARopp_mul_r Rsth Reqe ARth) ].
 
+Ltac gen_srewrite_sr Rsth Reqe ARth :=
+  repeat first
+     [ gen_reflexivity Rsth
+     | progress rewrite (ARopp_zero Rsth Reqe ARth)
+     | rewrite (ARadd_0_l ARth)
+     | rewrite (ARadd_0_r Rsth ARth)
+     | rewrite (ARmul_1_l ARth)
+     | rewrite (ARmul_1_r Rsth ARth)
+     | rewrite (ARmul_0_l ARth)
+     | rewrite (ARmul_0_r Rsth ARth)
+     | rewrite (ARdistr_l ARth)
+     | rewrite (ARdistr_r Rsth Reqe ARth)
+     | rewrite (ARadd_assoc ARth)
+     | rewrite (ARmul_assoc ARth) ].
+
 Ltac gen_add_push add Rsth Reqe ARth x :=
   repeat (match goal with
   | |- context [add (add ?y x) ?z] =>
-- 
cgit v1.2.3