]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/ng_refiner/nCicRefineUtil.mli
This commit patches the environment and the library so that their status is
[helm.git] / matitaB / components / ng_refiner / nCicRefineUtil.mli
index 22834237888e9d640c778fe3211ddbfa4986988c..f87c927d6b5fd71cb92b1ccef878b97a3627b8fa 100644 (file)
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-val alpha_equivalence : #NCic.status -> NCic.term -> NCic.term -> bool 
+val alpha_equivalence : #NCicEnvironment.status -> NCic.term -> NCic.term -> bool 
 
 val replace_lifting :
-  #NCic.status ->
+  #NCicEnvironment.status ->
   equality:((string * NCic.context_entry) list ->
             NCic.term -> NCic.term -> bool) ->
   context:(string * NCic.context_entry) list ->