Commented out code to optimize the case t1 vs t2 when t1 and t2 are both

meta closed. Why is it necessary, anyway?

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index edf116d17f08c94464887b7fb609301329e0f217..936d1ec8d0c3882e37aa444c3464e16140d26eb3 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -379,6 +379,16 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
          ~subst metasenv));
      if t1 === t2 then
        metasenv, subst
+(* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
+     else if
+      NCicUntrusted.metas_of_term subst context t1 = [] &&
+      NCicUntrusted.metas_of_term subst context t2 = []
+     then
+      if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
+       metasenv,subst
+      else
+       raise (UnificationFailure (lazy "Closed terms not convertible"))
+*)
      else
        match (t1,t2) with
        | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []