From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 2 Oct 2009 17:55:38 +0000 (+0000)
Subject: if the query has a completely flexible side, the empty result set is given
X-Git-Tag: make_still_working~3394
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1bff098f89787157818e2eb62acd6fcf4a2979d2;p=helm.git

if the query has a completely flexible side, the empty result set is given
---

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index e3112f3f2..1ea21dbcc 100644
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -247,6 +247,11 @@ let eq_class_of hdb t1 =
 ;;
 
 let look_for_hint hdb metasenv subst context t1 t2 =
+  if NDiscriminationTree.NCicIndexable.path_string_of t1 =
+          [Discrimination_tree.Variable] || 
+     NDiscriminationTree.NCicIndexable.path_string_of t2 =
+             [Discrimination_tree.Variable] then [] else begin
+
   debug(lazy ("KEY1: "^NCicPp.ppterm ~metasenv ~subst ~context t1));
   debug(lazy ("KEY2: "^NCicPp.ppterm ~metasenv ~subst ~context t2));
 (*
@@ -314,6 +319,7 @@ let look_for_hint hdb metasenv subst context t1 t2 =
     rc)));
 
   rc
+             end
 ;;
 
 let pp_hint t p =