From ed670d5c4b3d41955caa31a281087e341b1b7611 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 10 Jan 2006 12:00:24 +0000 Subject: [PATCH] Warning Y fixed. --- helm/ocaml/cic_disambiguation/disambiguate.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2