delift moved from cicSubstitution to cicUnification

[helm.git] / helm / ocaml / cic_unification / cicUnification.mli

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 2ec49722e412b951241f5275635c021ff830f90c..464927a2d05ff6738da9132c83698febb26d31a4 100644 (file)
--- 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