Back-porting from new Matita:

[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 fef24b2d5cad3b75c5da16b3356e6194ee56c861..4296102184017bff35f9afa84a7ceff5ea97de1c 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -18,6 +18,7 @@ exception AssertFailure of string Lazy.t;;
 val unify :
   #NRstatus.status ->
   ?test_eq_only:bool -> (* default: false *)
+  ?swap:bool -> (* default: false *)
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   NCic.term -> NCic.term ->
    NCic.metasenv * NCic.substitution
@@ -37,5 +38,11 @@ val delift_type_wrt_terms:
   NCic.term -> NCic.term list -> 
    NCic.metasenv * NCic.substitution * NCic.term
 
+val sortfy :
+    exn ->
+    NCic.metasenv ->
+    NCic.substitution ->
+    NCic.context ->
+    NCic.term -> NCic.metasenv * NCic.substitution * NCic.term
 
 val debug : bool ref