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

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 464927a2d..46f506710 100644
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -38,12 +38,31 @@ type substitution = (int * Cic.term) list
 (* unifies [t1] and [t2] in a context [context]. *)
 (* Only the metavariables declared in [metasenv] *)
 (* can be used in [t1] and [t2].                 *)
+(* The returned substitution can be directly     *)
+(* withouth first unwinding it.                  *)
 val fo_unif :
   Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
    substitution * Cic.metasenv
 
-(* apply_subst subst t                    *)
-(* applies the substitution [sust] to [t] *)
+(* fo_unif_subst metasenv subst context t1 t2    *)
+(* unifies [t1] and [t2] in a context [context]  *)
+(* and with [subst] as the current substitution  *)
+(* (i.e. unifies ([subst] [t1]) and              *)
+(* ([subst] [t2]) in a context                   *)
+(* ([subst] [context]) using the metasenv        *)
+(* ([subst] [metasenv])                          *)
+(* Only the metavariables declared in [metasenv] *)
+(* can be used in [t1] and [t2].                 *)
+(* [subst] and the substitution returned are not *)
+(* unwinded.                                     *)
+(*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la
+ cosa all'apply_subst!!!*)
+val fo_unif_subst :
+  substitution -> Cic.context -> Cic.metasenv -> Cic.term -> Cic.term ->
+   substitution * Cic.metasenv
+
+(* apply_subst subst t                     *)
+(* applies the substitution [subst] to [t] *)
 val apply_subst : substitution -> Cic.term -> Cic.term
 
 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)