diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:26:24 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:26:24 +0000 |
| commit | 50bbbf0502291688064c7ed59c7201f2efd0f0c5 (patch) | |
| tree | 151b989d4bccc4017fd0ab7021291d605a501b0f /plugins/firstorder/instances.ml | |
| parent | fb1b438ca1cdb206a1ad35d285e6fa8ea615d047 (diff) | |
Instances: generic equality on global_reference replaced by RefOrdered.compare
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14335 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/firstorder/instances.ml')
| -rw-r--r-- | plugins/firstorder/instances.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 881850365..16831d3ec 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -33,11 +33,11 @@ let compare_instance inst1 inst2= | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1 | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 -let compare_gr id1 id2= +let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else Pervasives.compare id1 id2 + else Libnames.RefOrdered.compare id1 id2 module OrderedInstance= struct |