From 611db91aed4ca748ac7effaf0024ba6d0d102810 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 28 Mar 2016 09:15:08 +0200
Subject: A mini-optimization for free in unification.ml: test in O(1)
 complexity comes before tests in O(n) complexity.

---
 pretyping/unification.ml | 6 ++++--
 1 file 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
-- 
cgit v1.2.3