The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT imag.fr>]

Hello everybody,

I have defined in Coq a higher-order abstract syntax for some expression 
language (in a Coq module "Syntax"):

Inductive expr (var:Type): Type :=
  | Var: var -> expr var
  ...

Definition eval (e: forall v, expr v) ....

Lemma eval_correctness (e: forall v, expr v): ...


My goal is to write a tactic in Ocaml to generate a Coq proof like 
"eval_correctness (fun v => f v) ..." for some "f"

But I do not understand how to use the Coq API to generate a valid sort 
"Type" for variable "v" in lambda-abstraction "fun (v:Type) => f v".
I am using Coq V8.5.2.

Currently, by imitating some files found in Coq plugins, I have written 
something like

Proofview.Goal.enter (fun gl ->
 let _eval_correctness = ... in
 let vid = Names.Id.of_string "v" in
 let evm = Proofview.Goal.sigma gl in
 let evm, vtype = Evd.new_sort_variable Evd.univ_flexible evm in
 let vtype = Term.mkSort vtype in
 let _f = .... (Term.mkVar vid) in
 let _e = Term.mkNamedLambda vid vtype f in
 ...
 let proof = Term.mkApp _eval_correctness [| _e; ... |] in
 Tacticals.New.tclTHENLIST
         [
           Proofview.Unsafe.tclEVARS evm;
           Proofview.V82.tactic (Tactics.exact_no_check proof);
         ])

But, when using this tactic inside a Coq module "TestTactic", I get the 
following error message:

Error: Illegal application:
The term "Syntax.Var" of type
 "forall var : Type, var -> Syntax.expr var"
cannot be applied to the terms
 "v" : "Type"
 "r4" : "v"
The 1st term has type "Type@{TestTactic.1}"
which should be coercible to "Type@{Syntax.1}".


How to correct my code above ?

Thanks.

Sylvain Boulmé.