diff options
| author | Hugo Herbelin | 2016-03-28 09:15:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-10 02:44:34 +0200 |
| commit | 611db91aed4ca748ac7effaf0024ba6d0d102810 (patch) | |
| tree | 57aab63db274c59522b5bc4f2268f41e4fa1dec1 | |
| parent | 7527751d9772656b4680df311546825cc2dd3d8f (diff) | |
A mini-optimization for free in unification.ml: test in O(1)
complexity comes before tests in O(n) complexity.
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index cdd543d255..21cf5548f2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1058,8 +1058,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in try let res = - if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n - || subterm_restriction opt flags then None + if subterm_restriction opt flags || + occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n + then + None else let sigma, b = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n |