diff options
| author | Pierre-Marie Pédrot | 2019-05-01 17:55:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-10 12:53:09 +0200 |
| commit | 1c4a11ee8b5b48b85911689e1bb93757359cdfca (patch) | |
| tree | 91ac3458b33ab108bb9d0e340f824fa205bc2149 /proofs/logic.ml | |
| parent | 4f3c70ad2deb8382130972c513cb19f0974580a8 (diff) | |
Fast-path for reordering of a single closed variable.
Doesn't seem to matter in practice, but it doesn't hurt either.
Diffstat (limited to 'proofs/logic.ml')
| -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 |