The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

It is an i of type mutual_inductive, which is an alias for MutInd.t. You can find MutInd.t in names.mli.

You can get that from the AST in this way:

| Construct (((i, _), _, _) ->

   let mutind_body = lookup_mind i env in ...

| Ind ((i, _), _) ->

   let mutind_body = lookup_mind i env in ...

To actually construct a name of an inductive type from a string is a little more complicated. I do it in this plugin in the function inductive_of_elim. It looks roughly like this:

let ind_label = Label.of_id (Id.of_string_soft ind_label_string) in

let ind_name = MutInd.make1 (KerName.make modpath dirpath ind_label) in

let body = lookup_mind ind_name env in ...

Where modpath and dirpath make the name fully-qualified.

I'm not sure why you have a string, but if you have a constant somewhere and just want to modify it a bit and then use that string to lookup_mind, your job is a little easier, because you can repr the fully qualified name:

let kn = Constant.canonical c in 

let (modpath, dirpath, label) = KerName.repr kn in ...

Anyways, I suggest looking at names.mli, or whatever the equivalent is in the newest Coq plugin API.