Printing of local contexts in argument position is reversed

[haselwarter]

Example

rule A type
rule B (a1 : A) (a2 : A) type
rule C ({x y : A} X type) type

let ex_wrong = C ({a b} (base.print (a,b) ; B a b))
let ex_okay  = ({a b : A} B a b)

Output:

andromeda.native  "argument_abstraction.m31"
Processing file argument_abstraction.m31
Rule A is postulated.
Rule B is postulated.
Rule C is postulated.
((x₀ : A ⊢ x₀ : A), (y₁ : A ⊢ y₁ : A))
val ex_wrong :> judgement = ⊢ C ({b a} B a b) type
val ex_okay :> judgement = ⊢ {a : A} {b : A} B a b type
Processed file argument_abstraction.m31

The abstraction in ex_wrong is reversed, we should get ⊢ C ({a b} B a b) type instead.

Another problem is that the call to base.print (a,b) seems to use the names x₀ and y₁ from the rule declaration of C instead of a₀ and b₁ from the binding abstraction.