New experimental commit: metavariables representation is changed again,

[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..2ec49722e412b951241f5275635c021ff830f90c 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -36,7 +36,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] *)