X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.mli;h=464927a2d05ff6738da9132c83698febb26d31a4;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=9fde49d9e22c6273a4ac46965498821de5b1eaf0;hpb=211f0ab4ee4c22c98147067987874b0b5a800b5b;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 9fde49d9e..464927a2d 100644
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -27,6 +27,9 @@ exception UnificationFailed
 exception Free
 exception OccurCheck
 
+val delift : 
+ Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
+
 (* The entry (i,t) in a substitution means that *)
 (* (META i) have been instantiated with t.      *)
 type substitution = (int * Cic.term) list
@@ -36,7 +39,8 @@ type substitution = (int * Cic.term) list
 (* Only the metavariables declared in [metasenv] *)
 (* can be used in [t1] and [t2].                 *)
 val fo_unif :
-  (int * Cic.term) list -> Cic.context -> Cic.term -> Cic.term -> substitution
+  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+   substitution * Cic.metasenv
 
 (* apply_subst subst t                    *)
 (* applies the substitution [sust] to [t] *)