X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.mli;h=83a59b64c550ad977d38148d7b19428fca9d2b72;hb=8e0e2b06cfc3fb3116e1fce632d9897fdbac9895;hp=a6ddfaeed2009b04f95c9c37dd3b3d5a1886b2b6;hpb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index a6ddfaeed..83a59b64c 100644
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -22,38 +22,18 @@ val unify :
   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.term -> 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 debug : bool ref