X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.mli;h=bbb96facbf573dac789db752b58eb556152406c9;hb=21ee96d317a4f0e7abfe76f697defe78acc10b94;hp=677454550f8aa1c38008d884872d3371c8bfedef;hpb=c515405206bfeb9f99d3e175b7f1e390ba299f28;p=helm.git

diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli
index 677454550..bbb96facb 100644
--- a/helm/software/components/ng_tactics/nCicElim.mli
+++ b/helm/software/components/ng_tactics/nCicElim.mli
@@ -11,5 +11,7 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-(* val mk_elims: NCic.obj -> NCic.obj list *)
 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