aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_trees.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_trees.ml')
-rw-r--r--proofs/proof_trees.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index a05464b00..86ec64c76 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -176,7 +176,7 @@ let prgl gl =
(str"[" ++ pgl ++ str"]" ++ spc ())
let pr_evgl gl =
- let phyps = pr_idl (ids_of_named_context gl.evar_hyps) in
+ let phyps = pr_idl (List.rev (ids_of_named_context gl.evar_hyps)) in
let pc = prterm gl.evar_concl in
hov 0 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pc ++ str"]")