The Coq mailing list

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

I reply to my own question. It is missing a typing pass that will solve 
the constraints.

  let sigma, typ = Typing.type_of env sigma def in
  Simple_declare.declare_definition ~poly:true (Names.Id.of_string 
"foo") sigma def

It could be emphasized more in the plugin tutorial as this pass is not 
necessary when fully defined terms without dangling universe are used 
and one may expect simple_declare to use the same typing algorithm again.

Pierre

On 23/04/2020 10:59, CREGUT Pierre IMT/OLN wrote:
> 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 []