aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-02-17 16:13:30 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-02-17 16:13:30 +0000
commitb63f3d7db6e23746165f2a8501dfc3b52351530b (patch)
tree66b0f0a7b6447c57b55b8e9261dee7015818cf78 /theories/FSets
parent308e5a317c6d7dff25d04138619a101e32768d26 (diff)
- 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
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FMapAVL.v5
-rw-r--r--theories/FSets/FMapInterface.v1
-rw-r--r--theories/FSets/FSetInterface.v1
3 files changed, 5 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).
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