The Coq mailing list

[CREGUT Pierre IMT/OLN <pierre.cregut AT orange.com>]

It is probably belonging to the FAQ level questions but I have not 
figured out where it is explained.

I am trying to create a very simple coq term in ml and make a top level 
definition :

    Definition foo := fun A:Type => prod A A.

I am using the Simple_declare.declare of plugin_tutorials/tuto1 (version 
8.11)

    let foo () =
      let env = Global.env() in
      let sigma = Evd.from_env env in
      let qprod = Libnames.qualid_of_string "Coq.Init.Datatypes.prod" in
      let sigma, sort = Evd.new_sort_variable Evd.univ_flexible sigma in
      let ty = EConstr.mkSort sort in
      let bd = Context.nameR (Names.Id.of_string "A") in
      let env = EConstr.push_rel 
(Context.Rel.Declaration.LocalAssum(bd,ty)) env in
      let sigma, prod =  EConstr.fresh_global env sigma 
(Constrintern.intern_reference qprod) in
      let def =  EConstr.mkLambda(bd, ty, EConstr.mkApp(prod, 
[|EConstr.mkRel 1; EConstr.mkRel 1|])) in
      Simple_declare.declare_definition ~poly:true (Names.Id.of_string 
"foo") sigma def

Clearly I am missing something A is of type Type@{Top.1}and it cannot be 
unified with Type@{prod.u0} from prod. How can I have a new universe 
scope in a few lines of code (for the standard 8.11 version, it seems 
the API is changing quickly). Is it in this part that I am missing 
something or in the use of UState.default_univ_decl in declare_definition ?

Best regards,

Pierre Crégut


simple_declare.ml:

let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body 
tyopt imps =
  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
      ~opaque ~poly sigma udecl ~types:tyopt ~body in
  let uctx = Evd.evar_universe_context sigma in
  let ubinders = Evd.universe_binders sigma in
  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
  DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps 
?hook_data

let declare_definition ~poly name sigma body =
  let udecl = UState.default_univ_decl in
  edeclare ~name ~poly ~scope:(DeclareDef.Global 
Declare.ImportDefaultBehavior)
    ~kind:Decls.(IsDefinition Definition) ~opaque:false sigma udecl 
body None []