The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I have an ml tactic that has a shell that looks like the following:

let arewrite : unit Proofview.tactic =

  Proofview.Goal.enter (fun gl ->

  let concl = Proofview.Goal.raw_concl gl in

  let e' = ...

  let (evm, env) = Lemmas.get_current_context() in

          Tacticals.New.tclTHENLIST

            [

              Equality.replace concl (build_predicate e' []) ;

            ]))

end

Inside it there is a call to a function build_predicate.  This function needs to build a predicate that contains a match clause.  I found that the record for a match clause contains a match info field.  I'm using the following two lines of code to build the match constructor:

    let ci = make_case_info Global.env ind RegularStyle in

    mkCase (ci, tterm, eterm, Array.of_list terms)

The "ci" field seems to contain information I need to pull from the global environment.  I was able to figure out the first and third parameters by looking at pieces of code in Coq.  However, I'm not able to figure out what to do with the "ind" field.  What do I fill in for ind?

                 - Ken