X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=667c50770536bb7187df52a2cc460991b32cf20f;hb=5104e38ee747fd1052ce21f3f9f2ecc778d590ba;hp=71f582211f5530a407ae661b8a2c028072e7ab73;hpb=727d6939c3f3ff1769ac1d11cad11d2e06433295;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 71f582211..667c50770 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -614,7 +614,8 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
       where_dom @ defs_dom
   | CicNotationPt.Ident (name, subst) ->
       (try
-        let index = find_in_context name context in
+        (* the next line can raise Not_found *)
+        ignore(find_in_context name context);
         if subst <> None then
           CicNotationPt.fail loc "Explicit substitutions not allowed here"
         else