instance fixed

[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 86f5fae1aafa86d8285d5149de8affa0c82d7a9a..fef24b2d5cad3b75c5da16b3356e6194ee56c861 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -23,7 +23,9 @@ val unify :
    NCic.metasenv * NCic.substitution
 
 (* this should be moved elsewhere *)
-val fix_sorts: NCic.term -> NCic.term
+val fix_sorts: 
+  NCic.metasenv -> NCic.substitution -> 
+    NCic.term -> NCic.metasenv * NCic.term
 
 (* delift_type_wrt_terms st m s c t args
  *   lift t (length args) 
@@ -35,3 +37,5 @@ val delift_type_wrt_terms:
   NCic.term -> NCic.term list -> 
    NCic.metasenv * NCic.substitution * NCic.term
 
+
+val debug : bool ref