From 499464cf99b8eb3c251a1666b929088ad3810b43 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 28 Oct 2009 15:36:45 +0000 Subject: [PATCH] Commented out code to optimize the case t1 vs t2 when t1 and t2 are both meta closed. Why is it necessary, anyway? --- helm/software/components/ng_refiner/nCicUnification.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 [] -- 2.39.2