This page gives information about programming in Coq Version 7. There is a similar page for programming in Coq Version 6

Coq programming frequently asked questions

• What are rawconstr terms?
• How do I obtain the type of term?
• How do I get a global reference from an identifier?
• How do I obtain a term from a string?
• How do I obtain the value associated to an identifier?
• How do I get rid of unbound de Bruijn indices?
• How do I obtain a type_judgement?

• What are rawconstr terms?

  Terms of type rawconstr are created in the first phase of translation from abstract syntax parse trees to constr terms, which really represent the core notion of calculus of construction terms. In rawconstr terms, implicit arguments and coercion are not inserted yet, but the mapping between identifiers and the object they represent and that should be present in the tables are already established.

• How do I obtain the type of term?

  If your term is already of type constr, you can call the function Typing.type_of. The extra arguments can be filled with (Global.env()) and Evd.empty.

  Here is an example:

  let global_type_of c = Typing.type_of (Global.env()) Evd.empty c
      

• How do I get a global reference from an identifier?

  construct a qualified identifier, using Nametab.make_qualid with an empty path as first argument.

  From a qualified identifier, just use Nametab.locate. It will raise the exception Not_found if the qualified identifier has not been entered in the tables.

• How do I obtain a term from a string (containing no periods ".")?

  You can first construct a qualified identifier by simply calling Names.make_qualid with an empty list for the dir_path (first argument). You can then obtain a global reference by using Nametab.locate. You can then construct a rawterm by simply using the Rawterm.RRef constructor, with Rawterm.dummy_loc as location. You can then obtain a constr by calling Pretyping.understand. The extra arguments may be Evd.empty for the argument of type evar_map and (Global.env()) for the argument of type env.

  Here is an example:

  let string_to_constr s = 
      Pretyping.understand
        Evd.empty (Global.env())
        (RRef(dummy_loc, Nametab.locate(make_qualid [] s)))
  	

  This solution does not work for sorts.

• How do I obtain the value associated to an identifier?

  You can always convert the identifier to a string and go back to the solution for strings.