fix_sorts (cfr. previous commit) used to break too many things.

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

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 47a59d4f2a88021c83e8c960de893aa71efbdafb..891c0738ecb9d9ee7b8e412c88526977918c562b 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -29,6 +29,9 @@ val unify :
   NCic.term -> NCic.term ->
    NCic.metasenv * NCic.substitution
 
+(* this should be moved elsewhere *)
+val fix_sorts: NCic.term -> NCic.term
+
 (* 
 exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;