diff options
| author | Matej Kosik | 2016-04-04 15:18:06 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-04-04 15:18:06 +0200 |
| commit | 7a825927ec81239777012533155dcce6d4defc18 (patch) | |
| tree | 211831d30e0a3905bb7b72900d9ae58866f32963 /printing/printer.ml | |
| parent | 6a1fb5ffbb9fd63fc0c2445b9391229a959e3608 (diff) | |
| parent | 16536fd734d6a7aaa6ff85f56cef629df74ce36a (diff) | |
Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunk
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 70b5ffcc41..22bc122bd5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -740,18 +740,17 @@ module OrderedContextObject = struct type t = context_object let compare x y = - match x , y with - | Variable i1 , Variable i2 -> Id.compare i1 i2 - | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2 - | Opaque k1 , Opaque k2 -> con_ord k1 k2 - | Transparent k1 , Transparent k2 -> con_ord k1 k2 - | Axiom _ , Variable _ -> 1 - | Opaque _ , Variable _ - | Opaque _ , Axiom _ -> 1 - | Transparent _ , Variable _ - | Transparent _ , Axiom _ - | Transparent _ , Opaque _ -> 1 - | _ , _ -> -1 + match x , y with + | Variable i1 , Variable i2 -> Id.compare i1 i2 + | Variable _ , _ -> -1 + | _ , Variable _ -> 1 + | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2 + | Axiom _ , _ -> -1 + | _ , Axiom _ -> 1 + | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Opaque _ , _ -> -1 + | _ , Opaque _ -> 1 + | Transparent k1 , Transparent k2 -> con_ord k1 k2 end module ContextObjectSet = Set.Make (OrderedContextObject) |