X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.mli;h=e8b4c7a8dff200f73d560e1af345bd4fcfcb7720;hb=4b85428dfb96b90fc8f00402b21affad9d99f905;hp=8366f1702286912ea50363a082ed249c2c17f452;hpb=43eef00462911f52ff53360e812b5b937097d05a;p=helm.git diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli index 8366f1702..e8b4c7a8d 100644 --- a/helm/software/components/ng_tactics/nCicElim.mli +++ b/helm/software/components/ng_tactics/nCicElim.mli @@ -11,4 +11,5 @@ (* $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