? when you show the examples of using your queries, please provide
  the link to the web interface of Whelp where the readers can check
  these examples themselves.
? some bibliography items ([5], [7], [12]) do not seem to be mentioned
  anywhere in the text of the article.
? please explain the content of the files returned by the queries
  in the form 'cic:/<some-path>.con', so that the readers who are
  less familiar with Coq can also understand it.

? Another annoying aspect of the paper is that while the approach is 
  claimed to be general, most of the problems the authors talk about (this
  is particularly true in the conclusion) seems to be system specific (Coq).

? Section 4:
  The approach of the meta-data is mostly presented as an alternative
  to other approaches. It seems very good at ruling out irrelevant
  theorems but a bit unprecise. We believe the approaches are just 
  complementary.   Applying first the meta-data and then some more 
  semantic technique seems an interesting and effective way of 
  producing more pertinent results.

? Section 5.3:
  In the case of Elim instead of trying to figure out if a theorem is
  an elimination theorem it would be much simpler to let the author of
  the theorem to indicate it explicitly (for example with a comment 
  schema as in Javadoc).
  In general, it seems a valuable feature to let database developers
  contribute to the meta-data generation.
  
? Section 5.4:
  An interesting question this section raises is how people name (or 
  should name) their theorems in a formal development. It seems that 
  your meta-data approach indicates an effective naming schema.

ROBA FATTA (+) O IGNORATA (=):

+ if there exist -> if there exists
= The real contribution of the paper is difficult to assess since a fair amount
  of what is presented here has already been published somewhere else. If the
  paper is finally accepted we strongly encourage the authors to restructure
  the paper and focus more on what is really new in what they present.