Merge of the V7_3_new_exportation branch.

[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 464927a2d05ff6738da9132c83698febb26d31a4..30094f7f2b7d2b7f0c6a1db9bd2d8794317a222f 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -38,12 +38,37 @@ 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
+
+(* unwind_subst metasenv subst                         *)
+(* unwinds [subst] w.r.t. itself.                      *)
+(* It can restrict some metavariable in the [metasenv] *)
+val unwind_subst : Cic.metasenv -> substitution -> substitution * Cic.metasenv
+
+(* apply_subst subst t                     *)
+(* applies the substitution [subst] to [t] *)
+(* [subst] must be already unwinded        *)
 val apply_subst : substitution -> Cic.term -> Cic.term
 
 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
@@ -55,5 +80,6 @@ val apply_subst : substitution -> Cic.term -> Cic.term
 (*  eta-expansions have been performed and the head of the new          *)
 (*  application has been unified with (META [meta_to_reduce]):          *)
 (*  during the unwinding the eta-expansions are undone.                 *)
+(* [subst] must be already unwinded                                     *)
 val apply_subst_reducing :
  substitution -> (int * int) option -> Cic.term -> Cic.term