From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 28 Oct 2009 15:36:45 +0000 (+0000)
Subject: Commented out code to optimize the case t1 vs t2 when t1 and t2 are both
X-Git-Tag: make_still_working~3237
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=499464cf99b8eb3c251a1666b929088ad3810b43;p=helm.git

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 edf116d17..936d1ec8d 100644
--- 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 []