From 1c4a11ee8b5b48b85911689e1bb93757359cdfca Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 May 2019 17:55:04 +0200
Subject: Fast-path for reordering of a single closed variable.

Doesn't seem to matter in practice, but it doesn't hurt either.
---
 proofs/logic.ml | 8 +++++---
 1 file 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
-- 
cgit v1.2.3