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 e3112f3f2c1d6df176dd19e10cbd527713f9b73c..1ea21dbcc0832d78551a956c8e660bcbbb877bdc 100644 (file)
--- 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 =