disambiguation now returns and takes in input the substitution

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.mli

diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli
index 9b10e3448cc05cbe52286639678525cc7d28e703..5d845eb1fe1526d2e713df641c566498a48439be 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.mli
+++ b/helm/software/components/ng_refiner/nCicRefiner.mli
@@ -11,8 +11,8 @@
 
 (* $Id$ *)
 
-exception RefineFailure of (Stdpp.location * string) Lazy.t;;
-exception Uncertain of (Stdpp.location * string) Lazy.t;;
+exception RefineFailure of Stdpp.location * (string Lazy.t);;
+exception Uncertain of Stdpp.location * (string Lazy.t);;
 exception AssertFailure of string Lazy.t;;
 
 val typeof :