From 980d315f7f6d5e05eabbda84f95e11bfa30a0033 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 16 Oct 2009 13:12:52 +0000 Subject: Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSets, and improve it As soon as you have a eq, a lt and a le (that may be lt\/eq, or (complement (flip (lt))) and a few basic properties over them, you can instantiate functor MakeOrderTac and gain an "order" tactic. See comments in the file for the scope of this tactic. NB: order doesn't call auto anymore. It only searches for a contradiction in the current set of (in)equalities (after the goal was optionally turned into hyp by double negation). Thanks to S. Lescuyer for his suggestions about this tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12397 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/MSets/MSetList.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/MSets/MSetList.v') diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index a6fc0affa..471b43e24 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -442,7 +442,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto; try sort_inf_in; try order. - right; intuition; inv; order. + right; intuition; inv; auto. Qed. Lemma equal_spec : -- cgit v1.2.3