Fast-path for reordering of a single closed variable.

Doesn't seem to matter in practice, but it doesn't hurt either.

1 files changed, 5 insertions, 3 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 76eb79df39..b79e1e6024 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -153,12 +153,14 @@ let reorder_context env sigma sign ord =
   step ord ords sign mt_q []
 
 let reorder_val_context env sigma sign ord =
+match ord with
+| [] | [_] ->
+  (* Single variable-free definitions need not be reordered *)
+  sign
+| _ :: _ :: _ ->
   let open EConstr in
   val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord)
 
-
-
-
 let check_decl_position env sigma sign d =
   let open EConstr in
   let x = NamedDecl.get_id d in