X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;fp=matitaB%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=162e172a4da9f38c767021d9f7fee9020d9ba7d6;hb=86b0a224bd9251ed22648de04bc0d00f11dbd0fc;hp=c39ac161d939d56dac961b2f0527589a07f8b759;hpb=e499c2e36d8a39c4749b8e0e34438b49532d15b8;p=helm.git

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index c39ac161d..162e172a4 100644
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -353,7 +353,7 @@ let disambiguate_nterm status expty context metasenv subst thing
           diff_term Stdpp.dummy_loc thing' ast) choices 
       in 
       raise (Ambiguous_input (find_diffs diffs)) 
-  | Disambiguate.Disamb_failure (l,_) ->
+  | Disambiguate.Disamb_failure l ->
       raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l))
   | _ -> assert false
 ;;
@@ -440,7 +440,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') =
           diff_obj Stdpp.dummy_loc obj ast) choices 
       in
       raise (Ambiguous_input (find_diffs diffs)) 
-  | Disambiguate.Disamb_failure (l,_) -> 
+  | Disambiguate.Disamb_failure l -> 
       raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l))
   | _ -> assert false
 ;;