snapshot (ported to new "typed" ids_to_inner_sort table)

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index a3a06f922d68ac446982334a4e03e7de31c204cd..b979e84c99f255aa313a3382106455d79d7702ad 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -375,7 +375,10 @@ let compiler32 (t: Patterns.t) success_k fail_k =
       k
     else if Patterns.are_empty t then begin
       (match t with
-      | _::_::_ -> warning "Ambiguous patterns"
+      | _::_::_ ->
+          (* optimization possible here: throw away all except one of the rules
+           * which lead to ambiguity *)
+          warning "Ambiguous patterns"
       | _ -> ());
       return_closure success_k
     end else