This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / ng_disambiguation / nCicDisambiguate.mli

diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
index 6f6bbd1a1b6413b2e2b50b0757d4a5e41a483d76..b63f8afaa37d54a257d547dbf4e83f149d02fa4e 100644 (file)
--- a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
+++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
@@ -55,4 +55,4 @@ val disambiguate_obj :
    NCic.substitution * NCic.obj)
   list * bool
 
-val disambiguate_path: #NCic.status -> NotationPt.term -> NCic.term
+val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term