new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[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 83a59b64c550ad977d38148d7b19428fca9d2b72..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)