rocq/backend/Order.v
Prolog's standard order of terms, and the sorted lists the Prolog compiler makes with it: sort/2, msort/2 and the ordsets of library(ordsets). The backend's plans list temporaries, live ranges and thunks in this order, so the Gallina backend sorts by it too.
For the ground terms of Term.v the order is: integers by value, then [ ], then atoms by character code, then compounds, by arity, then by name, then by their arguments from the left. A list that is not empty is the compound '[|]'(Head, Tail).
Comparing
The order of two atoms' names: by character code, a prefix first. Extract.v makes it OCaml's comparison of strings.
c, or d if c finds its two sides equal: one more key of a comparison by several.
As compare(Order, T, U): the standard order of the terms t and u.
Sorting
The sorted lists xs and ys merged; of two equal elements, xs's comes first.
A merge sort's stack of sorted runs: the run at depth i, if there is one, has 2^i elements.
The runs of a stack merged, the oldest first.
As msort(Xs, Sorted): xs in the order of cmp, equal elements in the order they had (a merge sort, as SWI-Prolog's is).
A sorted list with one element of each run of equal ones.
As sort(Xs, Sorted): xs sorted, without duplicates. Its results are ordsets.
As ord_union(Xs, Ys, Zs): the union of two ordsets.
As ord_subtract(Xs, Ys, Zs): the elements of the ordset xs that are not in the ordset ys.
Whether two ordsets of names are the same.