Code simplified.

[helm.git] / helm / software / components / ng_refiner / nCicUnification.mli

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 54ccf2143f479a2aec9251aba5296098f0fa8e0a..fef24b2d5cad3b75c5da16b3356e6194ee56c861 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -16,43 +16,26 @@ exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 val unify :
-  NCicUnifHint.db ->
+  #NRstatus.status ->
+  ?test_eq_only: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 debug : bool ref