The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

 Dear Yann,

>    add_lemma_rw K2Diam.

 K2Diam is a qualified name (i.e. a name of the form A.B.C.l where A,B and C
  are module names and l is a label).
 You can use Nametab.locate to get a global_reference out of a
  qualid. (A global_reference is a reference to a constant, or to an
  inductive type or ...)
 Then you check whether your global_reference is a ConstRef and you
  extract the constant. (The constant is the type of the references to
  constant definitions).
 Global.lookup_constant gives you the constant_body of your constant.
  (The constant_body holds the body and type of your definition).
 Declarations.const_body and Declarations.const_type gives you respectively 
the
  body and types of your constants, that are respectively a
  constr_substituted option (None for axioms) and a types (= constr).
 Declarations.force gives you the constr out of the constr_substituted.

 This is not the only way to do it. Other Coq developers may give you
 different advices.


>    Can you confirm kind_of_term is what I need to use ?

 Yes.

                                        Godd luck,
                                         C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------