X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.mli;h=46f506710553c119413df6f631c7633fd0fb278b;hb=0c62b48dd8d961279e780f6fbc2a915d18b77b92;hp=2ec49722e412b951241f5275635c021ff830f90c;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 2ec49722e..46f506710 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
@@ -35,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              *)