Factorized "find_equalities" in demodulation_tac.

[helm.git] / components / cic_disambiguation / disambiguate.ml

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index fbe191416a0185024ad68575688fb0bd3b91d511..fb4c338a447ee040ac8c4ecb63dfad86c149b31d 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -717,6 +717,10 @@ let domain_diff dom1 dom2 =
           (match elt with
               Symbol (symb',_) when symb = symb' -> true
             | _ -> false)
+       | Num i ->
+          (match elt with
+              Num _ -> true
+            | _ -> false)
        | item -> elt = item
      ) dom2
   in