X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.mli;h=4296102184017bff35f9afa84a7ceff5ea97de1c;hb=f1fc99e982ca6c9c939504c4dcf773edf582792a;hp=97976b7a308bbe34aae83a06b5b1f147ccd9b290;hpb=b68325537e9e42c5da370c9f053fa99dba8a55cd;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 97976b7a3..429610218 100644
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -16,42 +16,33 @@ exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 val unify :
+  #NRstatus.status ->
+  ?test_eq_only:bool -> (* default: false *)
+  ?swap:bool -> (* default: false *)
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   NCic.term -> NCic.term ->
    NCic.metasenv * NCic.substitution
 
-(* 
-exception UnificationFailure of string Lazy.t;;
-exception Uncertain of string Lazy.t;;
-exception AssertFailure of string Lazy.t;;
+(* this should be moved elsewhere *)
+val fix_sorts: 
+  NCic.metasenv -> NCic.substitution -> 
+    NCic.term -> NCic.metasenv * NCic.term
 
-(* fo_unif metasenv context t1 t2                *)
-(* 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 -> CicUniv.universe_graph -> 
-      Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+(* delift_type_wrt_terms st m s c t args
+ *   lift t (length args) 
+ *      [ rel 1 ... rel (len args) / lift (length args) (arg_1 .. arg_n) ]
+ *)      
+val delift_type_wrt_terms:
+  #NRstatus.status -> 
+  NCic.metasenv -> NCic.substitution -> NCic.context -> 
+  NCic.term -> NCic.term list -> 
+   NCic.metasenv * NCic.substitution * NCic.term
 
-(* 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 :
-  Cic.substitution -> Cic.context -> Cic.metasenv -> 
-    Cic.term -> Cic.term -> CicUniv.universe_graph ->
-      Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+val sortfy :
+    exn ->
+    NCic.metasenv ->
+    NCic.substitution ->
+    NCic.context ->
+    NCic.term -> NCic.metasenv * NCic.substitution * NCic.term
 
-      *)
+val debug : bool ref