X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.mli;h=398325df41fd08e28422b097b068e935d0e3d1e0;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=a195a2fd8d55cfcaf7bd88e7946655d3f0fa6fab;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_refiner/nCicMetaSubst.mli b/matita/components/ng_refiner/nCicMetaSubst.mli
index a195a2fd8..398325df4 100644
--- a/matita/components/ng_refiner/nCicMetaSubst.mli
+++ b/matita/components/ng_refiner/nCicMetaSubst.mli
@@ -19,6 +19,10 @@ val debug: bool ref
 (* the index of the last created meta *)
 val maxmeta: unit -> int
 
+(* Bad, this should be made functional and put in the status! *)
+val pushmaxmeta: unit -> unit
+val popmaxmeta: unit -> unit
+
 (* the delift function takes in input a metavariable index, a local_context
  * and a term t, and substitutes every subterm t' of t with its position 
  * (searched up-to unification) in
@@ -28,13 +32,16 @@ val maxmeta: unit -> int
  * the delift function is a term the implicit variable can be substituted with
  * to make the term [t] unifiable with the metavariable occurrence.  In general,
  * the problem is undecidable if we consider equivalence in place of alpha
- * convertibility. Our implementation, though, is even weaker than alpha
+ * convertibility.
+ * The old implementation, though, is even weaker than alpha
  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
  * (missing all the other cases). Does this matter in practice?
+ * The new experimental implementation, instead, works up to unification.
  * The metavariable index is the index of the metavariable that must not occur
  * in the term (for occur check).
  *)
 val delift : 
+  #NCic.status ->
   unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
     NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) -> 
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
@@ -46,6 +53,7 @@ val delift :
    additional (i.e. l' does not intersects l) positions whose restriction was
    forced because of type dependencies *)
 val restrict: 
+   #NCic.status ->
     NCic.metasenv ->
     NCic.substitution ->
     int -> int list ->
@@ -63,6 +71,7 @@ val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
 
 (* returns the resulting type, the metasenv and the arguments *)
 val saturate:
+   #NCic.status ->
     ?delta:int -> NCic.metasenv -> NCic.substitution -> 
     NCic.context -> NCic.term -> int ->
        NCic.term * NCic.metasenv * NCic.term list
@@ -71,3 +80,6 @@ val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind
 
 val is_out_scope_tag : NCic.meta_attrs -> bool
 val int_of_out_scope_tag : NCic.meta_attrs -> int
+
+val is_flexible:
+ #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool