X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=c04df8d37b076750fa5a269cfc2fb467141b4ed7;hb=a3ee89dab26307ce1cedc8041ede995a97d51446;hp=59ef3559264563ae6c2e2393e687eeb949df0af7;hpb=585469505faa97c21687128490828a1aabee94ee;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 59ef35592..c04df8d37 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -50,6 +50,9 @@ val ppterm: lowtac_status -> cic_term -> string
 val whd: 
       lowtac_status -> ?delta:int -> NCic.context -> cic_term -> 
         lowtac_status * cic_term 
+val normalize: 
+      lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
+        lowtac_status * cic_term 
 val typeof: 
       lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 val unify: 
@@ -60,9 +63,6 @@ val refine:
 val apply_subst:
   lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 
-(* CSC: this function must be moved elsewhere *)
-val apply_subst_obj: NCic.substitution -> NCic.obj_kind -> NCic.obj_kind
-
 val get_goalty: lowtac_status -> int -> cic_term
 val mk_meta: 
    lowtac_status -> ?name:string -> NCic.context ->