- Parameterize unification by two sets of transparent_state, one for open

term unification (for constant and variable delta unfolding) and one to
parameterize closed-term conversion. Most of the time conversion uses
full delta and unification does no delta. This fine-grain is used in
rewrite/setoid_rewrite, where only closed-term delta on global constants
is allowed.
- Interpret Hint Unfold as a directive for delta conversion in
auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints).
- Remove ad-hoc support for this in typeclasses. Now setoid_rewrite
works correctly w.r.t. the old version regarding local definitions.
- Fix closed bugs which needed updating due to syntax modifications.


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

3 files changed, 10 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
index bb475bdc2a..e330d46fd1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1411.v
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -1,4 +1,5 @@
 Require Import List.
+Require Import Program.
 
 Inductive Tree : Set :=
 | Br : Tree -> Tree -> Tree
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index 205e827982..e0c540f36e 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -10,7 +10,7 @@ Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x.
 Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z ->
 Seq x z.
 
-Add Relation (S a) Seq
+Add Parametric Relation a : (S a) Seq
  reflexivity proved by Seq_refl
  symmetry proved by Seq_sym
  transitivity proved by Seq_trans
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 12c92a8f7f..d6b7660b2d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -85,17 +85,17 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
       end
   end.
 
-Next Obligation. intro; apply H; inversion H0; subst; trivial. Defined.
-Next Obligation. intro; inversion H. Defined.
-Next Obligation. intro H; inversion H. Defined.
-Next Obligation. intro; inversion H; subst. Defined.
+Next Obligation. apply H; inversion H0; subst; trivial. reflexivity. Defined.
+Next Obligation. inversion H. Defined.
+Next Obligation. inversion H. Defined.
+Next Obligation. inversion H; subst. Defined.
 Next Obligation.
-  contradict H. inversion H; subst. assumption. 
+  contradict H. inversion H1; subst. assumption. 
   contradict H0; assumption. Defined.
 Next Obligation.
-  contradict H0. inversion H0; subst. assumption. Defined.
+  contradict H0. inversion H1; subst. assumption. Defined.
 Next Obligation.
-  contradict H. inversion H; subst. assumption. Defined.
+  contradict H. inversion H0; subst. assumption. Defined.
 Next Obligation.
-  contradict H. inversion H; subst; auto. Defined.
+  contradict H. inversion H0; subst; auto. Defined.