From a8299eca26974f287e0c14876dbaa947e0eaaf3c Mon Sep 17 00:00:00 2001 From: puech Date: Fri, 29 Jul 2011 14:26:31 +0000 Subject: Sequent: generic equality on ident replaced by id_ord git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14336 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/firstorder/sequent.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder/sequent.ml') diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 81bc355e0..42d5a4ce5 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -87,7 +87,7 @@ let compare_constr_int f t1 t2 = match kind_of_term t1, kind_of_term t2 with | Rel n1, Rel n2 -> n1 - n2 | Meta m1, Meta m2 -> m1 - m2 - | Var id1, Var id2 -> Pervasives.compare id1 id2 + | Var id1, Var id2 -> id_ord id1 id2 | Sort s1, Sort s2 -> Pervasives.compare s1 s2 | Cast (c1,_,_), _ -> f c1 t2 | _, Cast (c2,_,_) -> f t1 c2 -- cgit v1.2.3