diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:26:31 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:26:31 +0000 |
| commit | a8299eca26974f287e0c14876dbaa947e0eaaf3c (patch) | |
| tree | 42dbe60fda20c6bef35385e0227066cecf7da96b /plugins/firstorder/sequent.ml | |
| parent | 50bbbf0502291688064c7ed59c7201f2efd0f0c5 (diff) | |
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
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |