diff options
| -rw-r--r-- | proofs/logic.ml | 8 |
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 |