1) new tactic normalize (low-level function implemented in

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

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 0653223af39fcae890932ec36878835485a572c2..c04df8d37b076750fa5a269cfc2fb467141b4ed7 100644 (file)
--- 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: