From 23e71d44504395ecefbee165ce7144bdf4fafe8f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 5 Mar 2024 11:45:21 +0100 Subject: [PATCH] The using "using" clause moved from CInfo.t to Info.t. --- src/coq_elpi_builtins.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 19ff4b470..34b14b242 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1944,8 +1944,8 @@ Supported attributes: let using = using_from_string s in definition_using (get_global_env state) sigma ~fixnames:[] ~using ~terms:types) options.using in - let cinfo = Declare.CInfo.make ?using ~name:(Id.of_string id) ~typ:types ~impargs:[] () in - let info = Declare.Info.make ~scope ~kind ~poly ~udecl () in + let cinfo = Declare.CInfo.make ~name:(Id.of_string id) ~typ:types ~impargs:[] () in + let info = Declare.Info.make ~scope ~kind ~poly ~udecl ?using () in let used = Univ.Level.Set.union