Bug fixed: aliases for numbers were no longer handled correctly (since 0 was

a wildcard only for symbols).

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index fbe191416a0185024ad68575688fb0bd3b91d511..fb4c338a447ee040ac8c4ecb63dfad86c149b31d 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/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