X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.mli;h=bbb96facbf573dac789db752b58eb556152406c9;hb=186638106f23401e88e512a4a6dfd07d73d8be04;hp=e8b4c7a8dff200f73d560e1af345bd4fcfcb7720;hpb=72b4799ea220bc54dc27b34fdb863f1ee6fc9e08;p=helm.git

diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli
index e8b4c7a8d..bbb96facb 100644
--- a/helm/software/components/ng_tactics/nCicElim.mli
+++ b/helm/software/components/ng_tactics/nCicElim.mli
@@ -13,3 +13,5 @@
 
 val mk_elims: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
 val mk_projections: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
+val ast_of_sort : 
+  NCic.sort -> [> `NCProp of string | `NType of string | `Prop ]  * string