]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nCicUnification.mli
param "slir" to call the new auto
[helm.git] / helm / software / components / ng_refiner / nCicUnification.mli
index 954f56e58ee86a895acdd0b074cab1525cfcc492..4296102184017bff35f9afa84a7ceff5ea97de1c 100644 (file)
@@ -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