Initial revision

[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 9fde49d9e22c6273a4ac46965498821de5b1eaf0..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
@@ -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] *)