Here we show the procedure to follow to add the recognition of
a new syntactical form.

Form to recognize in the model:

Lemma existsDec : (l:(list A)){(list_exists l)}+{~(list_exists l)}.

1. cd V7 ; grep "Lemma" */*.ml4
   the result should be one or a few files. In this case the
   only file is parsing/g_vernac.ml4. In the case of many files,
   only one is the good one.
2. open the file and search for Lemma:
   thm_tok:
    [ [ "Theorem" -> <:ast< "THEOREM" >>
      | IDENT "Lemma" -> <:ast< "LEMMA" >>
      | IDENT "Fact" -> <:ast< "FACT" >>
      | IDENT "Remark" -> <:ast< "REMARK" >>
      | IDENT "Decl" -> <:ast< "DECL" >> ] ]

   so a Lemma is mapped into an ast of phylum thm_tok.
   Let's search for thm_tok. Many occurrences are found,
   but the only one that matches the form to recognize is

  gallina:
    (* Definition, Goal *)
    [ [ thm = thm_tok; id = identarg; ":"; c = constrarg ->
          <:ast< (StartProof $thm $id $c) >>

  So the ast created is tagged StartProof
3. grep "StartProof" */*.ml   (usually toplevel/...)
   Open the file and search for StartProof.
   This is found:
    let _ =
  add "StartProof"
    (function
       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
           ...
4. edit xmltheoryentries.ml and copy the entry for another rule,
   substituting StartProof as the parameter for set_hook and
   using the above match (with V. added where appropriate) after function:

let module V = Vernacinterp in
 set_hook "StartProof"
  (function
      [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
       ???
    | _ -> fail ()
  )
;;

    Finally, write OCaml code to print to XML the availables interesting
    infos. In our case the code becomes

let module V = Vernacinterp in
 set_hook "StartProof"
  (function
      [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
       IXml.output
        (Xml.xml_empty
          "THEOREM"
          ["uri", Names.string_of_id s ^ ".con"; "as",kind]
        )
    | _ -> fail ()
  )
;;

     IXml.output should always be present and the code inside
     (that is simply XML written in OCaml form) should be changed.
     The syntax is
        Xml.xml_empty "name" ["att1","value1" ; ... ; "attn","valuen"]
     to create an empty element name with attributes att1 ... attn.
     To create a non-empty element, use
        Xml.xml_nempty "name" ["att1","value1" ; ... ; "attn","valuen"]
         stream
     where stream is an OCaml stream of other XML elements, as:
       * another Xml.xml_nempty 
       * an Xml.xml_empty
       * [< stream1 ; ... ; streamk >]