* First implementation of CicRefine

[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 46f506710553c119413df6f631c7633fd0fb278b..30094f7f2b7d2b7f0c6a1db9bd2d8794317a222f 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -61,8 +61,14 @@ 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              *)
@@ -74,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