more tests

[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 74b5366db396b5dee570fc213415a35f1764cca8..59ef3559264563ae6c2e2393e687eeb949df0af7 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -60,6 +60,8 @@ 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: