Refine can now also raise Uncertain. The exception is raised every

[helm.git] / helm / ocaml / cic_unification / cicRefine.mli

diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index 18884bb12983c3ea86bf510c293ef16b1528c34b..338f50663dba12ac272dcbbc2ce9246e9cbb7074 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.mli
+++ b/helm/ocaml/cic_unification/cicRefine.mli
@@ -24,6 +24,7 @@
  *)
 
 exception NotRefinable of string
+exception Uncertain of string
 exception WrongUriToConstant of string
 exception WrongUriToVariable of string
 exception WrongUriToMutualInductiveDefinitions of string