- Use transparency information all the way through unification and

conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.


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

5 files changed, 7 insertions, 3 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 516015ab9..5a9b5d898 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -37,6 +37,7 @@ Open Local Scope lazy_bool_scope.
 Open Local Scope Int_scope.
 
 Definition key := X.t.
+Hint Transparent key.
 
 (** * Trees *)
 
@@ -821,7 +822,7 @@ Proof.
  intros l x e r; functional induction (bal l x e r); intros; clearf;
  inv bst; repeat apply create_bst; auto; unfold create; try constructor;
  (apply lt_tree_node || apply gt_tree_node); auto;
- (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
+ (eapply lt_tree_trans || eapply gt_tree_trans); eauto. 
 Qed.
 Hint Resolve bal_bst.
 
@@ -1331,7 +1332,7 @@ Proof.
  inversion_clear H.
  destruct H7; simpl in *.
  order.
- destruct (elements_aux_mapsto r acc x e0); intuition eauto.
+ destruct (elements_aux_mapsto r acc x e0); intuition eauto. 
 Qed.
 
 Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s).
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 252e67930..4d89b562d 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -56,6 +56,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
 Module Type WSfun (E : DecidableType).
 
   Definition key := E.t.
+  Hint Transparent key.
 
   Parameter t : Type -> Type.
   (** the abstract type of maps *)
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index a23263890..a03611193 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -251,6 +251,7 @@ Module Type WSfun (E : DecidableType).
 
   End Spec.
 
+  Hint Transparent elt.
   Hint Resolve mem_1 equal_1 subset_1 empty_1
     is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
     remove_2 singleton_2 union_1 union_2 union_3
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 253267fc8..5d17dd3f1 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -46,6 +46,7 @@ Local Open Scope Int_scope.
 Local Open Scope lazy_bool_scope.
 
 Definition elt := X.t.
+Hint Transparent elt.
 
 (** ** Trees
 
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index 67ed77981..b046e383d 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -96,7 +96,7 @@ Definition pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
 (** Injectivity *)
 
 Lemma pow_inj_l : forall a b c, c~=0 -> a^c == b^c -> a == b.
-Proof. intros; eapply pow_inj_l; eauto; auto'. auto'. Qed.
+Proof. intros; eapply pow_inj_l; eauto; auto'. Qed.
 
 Lemma pow_inj_r : forall a b c, 1<a -> a^b == a^c -> b == c.
 Proof. intros; eapply pow_inj_r; eauto; auto'. Qed.