Many changes

[helm.git] / matita / components / ng_tactics / nTacStatus.mli

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index da50ea2ac17d435c3ffc8c0db6ac0eae9c3253a9..44c95304519fdecdbe787e9081e8957c39e54e21 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.mli
+++ b/matita/components/ng_tactics/nTacStatus.mli
@@ -85,6 +85,8 @@ val whd:
 val normalize: 
  #pstatus as 'status -> ?delta:int -> NCic.context -> cic_term ->
   'status * cic_term 
+val are_convertible: 
+ #pstatus as 'status -> NCic.context -> cic_term -> cic_term -> 'status * bool
 val typeof: 
  #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
 val unify: