The Coq mailing list

[Anamaria Martins-Moreira <Anamaria.Martins-Moreira AT loria.fr>]

 Hi,

 I am a novice user of Coq and I am trying to define a grammar
 extension where I extract the type of a term given by the user:

 Grammar vernac vernac :=
  toto [ "Toto" constr:constr($term) "."] ->
          let $type = ...(type of $term) in
                                           (action usinf $term and $type)


 My question is how can I do it? (apparently I cannot call Check
 inside the let, or maybe there is a special way to do it)

 Thanks for any information,
 Anamaria