- 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

1 files changed, 3 insertions, 2 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).