Since I guess the divergence bug is fixed, I activate the test again.

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

diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli
index 677454550f8aa1c38008d884872d3371c8bfedef..e8b4c7a8dff200f73d560e1af345bd4fcfcb7720 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.mli
+++ b/helm/software/components/ng_tactics/nCicElim.mli
@@ -11,5 +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