X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.mli;h=464927a2d05ff6738da9132c83698febb26d31a4;hb=0328c0e2938ce714d5d7358afdca00195577198e;hp=2ec49722e412b951241f5275635c021ff830f90c;hpb=14a126b578b2c9a26d849553c65cec5e381df8fb;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 2ec49722e..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