From 5e32e4af5f7120b853dc112f631d5cb6526549e2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1s=20D=C3=ADaz?= Date: Mon, 24 Nov 2025 14:30:10 +0100 Subject: [PATCH] Adapt to rocq-prover/rocq#21195 (Univ.Constraints -> UnivConstraints) fixup optcomp Fix overlay for elimination-constraints Fix overlay Fix overlay, test on 9.1 Fix unused opens Try to fix the weird issue with univ_binder_compat_820 Typo Another unused open Another try --- src/rocq_elpi_HOAS.ml | 124 ++++++++++++++++++++++++++--------- src/rocq_elpi_HOAS.mli | 43 ++++++++++-- src/rocq_elpi_arg_HOAS.ml | 43 ++++++++---- src/rocq_elpi_arg_HOAS.mli | 12 ++++ src/rocq_elpi_arg_syntax.mlg | 16 +++-- src/rocq_elpi_builtins.ml | 115 ++++++++++++++++++-------------- 6 files changed, 251 insertions(+), 102 deletions(-) diff --git a/src/rocq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml index d785710a1..f4058b514 100644 --- a/src/rocq_elpi_HOAS.ml +++ b/src/rocq_elpi_HOAS.ml @@ -108,9 +108,13 @@ let constraint_eq u1 u2 = let open UnivProblem in ULe (u1, u2) +[%%if coq = "9.0" || coq = "9.1"] let add_constraints state c = S.update (Option.get !pre_engine) state (fun ({ sigma } as x) -> { x with sigma = Evd.add_universe_constraints sigma c }) - +[%%else] +let add_constraints state c = S.update (Option.get !pre_engine) state (fun ({ sigma } as x) -> + { x with sigma = Evd.add_constraints sigma c }) +[%%endif] let add_universe_constraint state c = let open UnivProblem in try add_constraints state (Set.singleton c) @@ -204,23 +208,92 @@ let universe_level_variable = end } -let universe_constraint : Univ.univ_constraint API.Conversion.t = +[%%if coq = "9.0" || coq = "9.1"] +type univ_cst = Univ.univ_constraint +type univ_csts = Univ.Constraints.t +type univ_ctx_set = Univ.ContextSet.t + +let univ_lt = Univ.Lt +let univ_le = Univ.Le +let univ_eq = Univ.Eq +let univ_csts_of_list = Univ.Constraints.of_list +let univ_csts_to_list = Univ.Constraints.elements +let evd_merge_ctx_set rigid = Evd.merge_sort_context_set rigid +let subst_univs_constraints = Univ.subst_univs_level_constraints +let univs_of_csts = UVars.UContext.constraints +let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance = + let open UState in + { univdecl_qualities = []; + univdecl_extensible_instance; + univdecl_extensible_qualities = false; + univdecl_extensible_constraints; + univdecl_constraints; + univdecl_instance} +let default_univ_decl = UState.default_univ_decl +let dest_udecl ({ UState.univdecl_instance ; univdecl_constraints } : UState.universe_decl) = + univdecl_instance, univdecl_constraints + +let universe_constraint : univ_cst API.Conversion.t = let open API.Conversion in let open API.AlgebraicData in declare { ty = TyName "univ-constraint"; doc = "Constraint between two universes level variables"; pp = (fun fmt _ -> Format.fprintf fmt ""); constructors = [ K("lt","",A(universe_level_variable,A(universe_level_variable,N)), - B (fun u1 u2 -> (u1,Univ.Lt,u2)), + B (fun u1 u2 -> (u1,univ_lt,u2)), M (fun ~ok ~ko -> function (l1,Univ.Lt,l2) -> ok l1 l2 | _ -> ko ())); K("le","",A(universe_level_variable,A(universe_level_variable,N)), - B (fun u1 u2 -> (u1,Univ.Le,u2)), + B (fun u1 u2 -> (u1,univ_le,u2)), M (fun ~ok ~ko -> function (l1,Univ.Le,l2) -> ok l1 l2 | _ -> ko ())); K("eq","",A(universe_level_variable,A(universe_level_variable,N)), - B (fun u1 u2 -> (u1,Univ.Eq,u2)), + B (fun u1 u2 -> (u1,univ_eq,u2)), M (fun ~ok ~ko -> function (l1,Univ.Eq,l2) -> ok l1 l2 | _ -> ko ())) ] } |> API.ContextualConversion.(!<) +[%%else] +type univ_cst = Univ.UnivConstraint.t +type univ_csts = Univ.UnivConstraints.t +type univ_ctx_set = PConstraints.ContextSet.t +let univ_lt = Univ.UnivConstraint.Lt +let univ_le = Univ.UnivConstraint.Le +let univ_eq = Univ.UnivConstraint.Eq +let univ_csts_of_list = Univ.UnivConstraints.of_list +let univ_csts_to_list = Univ.UnivConstraints.elements +let evd_merge_ctx_set rigid = Evd.merge_sort_context_set rigid QGraph.Internal +let subst_univs_constraints x = UVars.subst_univs_constraints (Sorts.QVar.Map.empty,x) +let univs_of_csts x = PConstraints.univs @@ UVars.UContext.constraints x +let mk_universe_decl sort_poly_decl_extensible_instance sort_poly_decl_extensible_constraints sort_poly_decl_univ_constraints sort_poly_decl_instance = + let open UState in + { sort_poly_decl_qualities = []; + sort_poly_decl_extensible_instance; + sort_poly_decl_elim_constraints = Sorts.ElimConstraints.empty; + sort_poly_decl_extensible_qualities = false; + sort_poly_decl_extensible_constraints; + sort_poly_decl_univ_constraints; + sort_poly_decl_instance} +let default_univ_decl = UState.default_sort_poly_decl +let dest_udecl ({ UState.sort_poly_decl_instance ; sort_poly_decl_univ_constraints } : UState.sort_poly_decl) = + sort_poly_decl_instance, sort_poly_decl_univ_constraints + +let universe_constraint : univ_cst API.Conversion.t = + let open API.Conversion in let open API.AlgebraicData in declare { + ty = TyName "univ-constraint"; + doc = "Constraint between two universes level variables"; + pp = (fun fmt _ -> Format.fprintf fmt ""); + constructors = [ + K("lt","",A(universe_level_variable,A(universe_level_variable,N)), + B (fun u1 u2 -> (u1,univ_lt,u2)), + M (fun ~ok ~ko -> function (l1,Univ.UnivConstraint.Lt,l2) -> ok l1 l2 | _ -> ko ())); + K("le","",A(universe_level_variable,A(universe_level_variable,N)), + B (fun u1 u2 -> (u1,univ_le,u2)), + M (fun ~ok ~ko -> function (l1,Univ.UnivConstraint.Le,l2) -> ok l1 l2 | _ -> ko ())); + K("eq","",A(universe_level_variable,A(universe_level_variable,N)), + B (fun u1 u2 -> (u1,univ_eq,u2)), + M (fun ~ok ~ko -> function (l1,Univ.UnivConstraint.Eq,l2) -> ok l1 l2 | _ -> ko ())) + ] +} |> API.ContextualConversion.(!<) +[%%endif] + let universe_variance : (Univ.Level.t * UVars.Variance.t option) API.Conversion.t = let open API.Conversion in let open API.AlgebraicData in declare { @@ -243,8 +316,8 @@ let universe_variance : (Univ.Level.t * UVars.Variance.t option) API.Conversion. ] } |> API.ContextualConversion.(!<) -type universe_decl = (Univ.Level.t list * bool) * (Univ.Constraints.t * bool) -type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list * bool) * (Univ.Constraints.t * bool) +type universe_decl = (Univ.Level.t list * bool) * (univ_csts * bool) +type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list * bool) * (univ_csts * bool) type any_universe_decl = | NonCumul of universe_decl @@ -257,11 +330,11 @@ let universe_decl : any_universe_decl API.Conversion.t = pp = (fun fmt _ -> Format.fprintf fmt ""); constructors = [ K("upoly-decl","",A(list universe_level_variable,A(bool,A(list universe_constraint,A(bool,N)))), - B (fun x sx y sy-> NonCumul ((x,sx),(Univ.Constraints.of_list y,sy))), - M (fun ~ok ~ko -> function NonCumul ((x,sx),(y,sy)) -> ok x sx (Univ.Constraints.elements y) sy | Cumul _ -> ko ())); + B (fun x sx y sy-> NonCumul ((x,sx),(univ_csts_of_list y,sy))), + M (fun ~ok ~ko -> function NonCumul ((x,sx),(y,sy)) -> ok x sx (univ_csts_to_list y) sy | Cumul _ -> ko ())); K("upoly-decl-cumul","",A(list universe_variance,A(bool,A(list universe_constraint,A(bool,N)))), - B (fun x sx y sy -> Cumul ((x,sx),(Univ.Constraints.of_list y,sy))), - M (fun ~ok ~ko -> function Cumul ((x,sx),(y,sy)) -> ok x sx (Univ.Constraints.elements y) sy | NonCumul _ -> ko ())) + B (fun x sx y sy -> Cumul ((x,sx),(univ_csts_of_list y,sy))), + M (fun ~ok ~ko -> function Cumul ((x,sx),(y,sy)) -> ok x sx (univ_csts_to_list y) sy | NonCumul _ -> ko ())) ] } |> API.ContextualConversion.(!<) @@ -889,8 +962,8 @@ module CoqEngine_HOAS : sig (* when the env changes under the hood, we can adapt sigma or drop it but keep its constraints *) - val from_env_keep_univ_of_sigma : uctx:Univ.ContextSet.t -> env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine - val from_env_keep_univ_and_sigma : uctx:Univ.ContextSet.t -> env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine + val from_env_keep_univ_of_sigma : uctx:univ_ctx_set -> env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine + val from_env_keep_univ_and_sigma : uctx:univ_ctx_set -> env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine end = struct @@ -1690,11 +1763,11 @@ let body_of_constant state c inst_opt = S.update_return engine state (fun x -> let c, ctx = UnivGen.fresh_global_instance x.global_env (ConstRef c) ?names:inst_opt in let c, inst = Constr.destConst c in let bo = Vars.subst_instance_constr inst bo in - let sigma = Evd.merge_sort_context_set Evd.univ_rigid x.sigma ctx in + let sigma = evd_merge_ctx_set Evd.univ_rigid x.sigma ctx in let sigma = match priv with | Opaqueproof.PrivateMonomorphic () -> sigma | Opaqueproof.PrivatePolymorphic ctx -> - let ctx = Util.on_snd (Univ.subst_univs_level_constraints (snd (UVars.make_instance_subst inst))) ctx in + let ctx = Util.on_snd (subst_univs_constraints (snd (UVars.make_instance_subst inst))) ctx in Evd.merge_context_set Evd.univ_rigid sigma ctx in { x with sigma }, (Some (EConstr.of_constr bo), Some inst) @@ -1852,7 +1925,7 @@ let in_coq_poly_gref ~depth ~origin ~failsafe s t i = s, u, [] with Not_found -> let u, ctx = UnivGen.fresh_global_instance (get_global_env s) t in - let s = update_sigma s (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx) in + let s = update_sigma s (fun sigma -> evd_merge_ctx_set UState.univ_flexible_alg sigma ctx) in let u = match C.kind u with | C.Const (_, u) -> u @@ -2943,9 +3016,9 @@ let universes_of_term state t = let sigma = get_sigma state in snd (EConstr.universes_of_constr sigma t) -let universes_of_udecl state ({ UState.univdecl_instance ; univdecl_constraints } : UState.universe_decl) = - let used1 = univdecl_instance in - let used2 = List.map (fun (x,_,y) -> [x;y]) (Univ.Constraints.elements univdecl_constraints) in +let universes_of_udecl state udecl = + let used1, csts = dest_udecl udecl in + let used2 = List.map (fun (x,_,y) -> [x;y]) (univ_csts_to_list csts) in let used = List.fold_right Univ.Level.Set.add used1 Univ.Level.Set.empty in let used = List.fold_right Univ.Level.Set.add (List.flatten used2) used in used @@ -2966,18 +3039,9 @@ let name_universe_level state l = ) -let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance = - let open UState in - { univdecl_qualities = []; - univdecl_extensible_instance; - univdecl_extensible_qualities = false; - univdecl_extensible_constraints; - univdecl_constraints; - univdecl_instance} - let poly_cumul_udecl_variance_of_options state options = match options.universe_decl with - | NotUniversePolymorphic -> state, false, false, UState.default_univ_decl, [| |] + | NotUniversePolymorphic -> state, false, false, default_univ_decl, [| |] | Cumulative ((univ_lvlt_var,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) -> let univdecl_instance, variance = List.split univ_lvlt_var in state, true, true, @@ -3536,7 +3600,7 @@ let upoly_decl_of ~depth state ~loose_udecl mie = if not (CArray.is_empty qvars) then nYI "sort poly inductives" else let state, vars = CArray.fold_left_map (fun s l -> fst (name_universe_level s l), l) state vars in - let csts = UVars.UContext.constraints uc in + let csts = univs_of_csts uc in begin match mie.mind_entry_variance with | None -> let state, up, gls = universe_decl.API.Conversion.embed ~depth state (NonCumul ((Array.to_list vars,loose_udecl),(csts,loose_udecl))) in diff --git a/src/rocq_elpi_HOAS.mli b/src/rocq_elpi_HOAS.mli index d4c3639b5..f389ffab2 100644 --- a/src/rocq_elpi_HOAS.mli +++ b/src/rocq_elpi_HOAS.mli @@ -24,8 +24,19 @@ type uinstanceoption = | VarInstance of (FlexibleData.Elpi.t * RawData.term list * inv_rel_key) (* a variable was provided, the command will compute the instance to unify with it *) -type universe_decl = (Univ.Level.t list * bool) * (Univ.Constraints.t * bool) -type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list * bool) * (Univ.Constraints.t * bool) +[%%if coq = "9.0" || coq = "9.1"] +type univ_cst = Univ.univ_constraint +type univ_csts = Univ.Constraints.t +type univ_ctx_set = Univ.ContextSet.t +[%%else] +type univ_cst = Univ.UnivConstraint.t +type univ_csts = Univ.UnivConstraints.t +type univ_ctx_set = PConstraints.ContextSet.t +[%%endif] + +type universe_decl = (Univ.Level.t list * bool) * (univ_csts * bool) +type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list * bool) * (univ_csts * bool) + type universe_decl_option = | NotUniversePolymorphic | Cumulative of universe_decl_cumul @@ -115,10 +126,14 @@ type record_field_spec = { name : Name.t; is_coercion : coercion_status; is_cano val lp2inductive_entry : depth:int -> empty coq_context -> constraints -> State.t -> term -> State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals -[%%else] +[%%elif coq = "9.1"] val lp2inductive_entry : depth:int -> empty coq_context -> constraints -> State.t -> term -> State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals +[%%else] +val lp2inductive_entry : + depth:int -> empty coq_context -> constraints -> State.t -> term -> + State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * PConstraints.ContextSet.t * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals [%%endif] [%%if coq = "9.0"] @@ -222,7 +237,12 @@ val in_elpiast_primitive : loc:Ast.Loc.t -> primitive_value -> Ast.Term.t val uinstance : UVars.Instance.t Conversion.t +[%%if coq = "9.0" || coq = "9.1"] val universe_constraint : Univ.univ_constraint Conversion.t +[%%else] +val universe_constraint : Univ.UnivConstraint.t Conversion.t +[%%endif] + val universe_variance : (Univ.Level.t * UVars.Variance.t option) Conversion.t type any_universe_decl = | NonCumul of universe_decl @@ -306,11 +326,16 @@ val body_of_constant : State.t -> Names.Constant.t -> UVars.Instance.t option -> State.t * EConstr.t option * UVars.Instance.t option -val grab_global_env : uctx:Univ.ContextSet.t -> State.t -> State.t val grab_global_env_drop_univs_and_sigma : State.t -> State.t val grab_global_env_drop_sigma : State.t -> State.t -val grab_global_env_drop_sigma_keep_univs : uctx:Univ.ContextSet.t -> State.t -> State.t +[%%if coq = "9.0" || coq = "9.1"] +val grab_global_env : uctx:Univ.ContextSet.t -> State.t -> State.t +val grab_global_env_drop_sigma_keep_univs : uctx:Univ.ContextSet.t -> State.t -> State.t +[%%else] +val grab_global_env : uctx:PConstraints.ContextSet.t -> State.t -> State.t +val grab_global_env_drop_sigma_keep_univs : uctx:PConstraints.ContextSet.t -> State.t -> State.t +[%%endif] val mk_decl : depth:int -> Name.t -> ty:term -> term (* Adds an Arg for the normal form with ctx_len context entry vars in scope *) @@ -347,10 +372,16 @@ val force_level_of_universe : state -> Univ.Universe.t -> state * Univ.Level.t * val purge_algebraic_univs_sort : state -> EConstr.ESorts.t -> state * Sorts.t val ideclc : constant val uideclc : constant -val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * Entries.variance_entry val merge_universe_context : state -> UState.t -> state val restricted_sigma_of : Univ.Level.Set.t -> state -> Evd.evar_map val universes_of_term : state -> EConstr.t -> Univ.Level.Set.t + +[%%if coq = "9.0" || coq = "9.1"] +val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * Entries.variance_entry val universes_of_udecl : state -> UState.universe_decl -> Univ.Level.Set.t +[%%else] +val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.sort_poly_decl * Entries.variance_entry +val universes_of_udecl : state -> UState.sort_poly_decl -> Univ.Level.Set.t +[%%endif] val mind_record : Declarations.mind_specif -> Declarations.record_info diff --git a/src/rocq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml index d36aa30cf..9259dc10a 100644 --- a/src/rocq_elpi_arg_HOAS.ml +++ b/src/rocq_elpi_arg_HOAS.ml @@ -138,6 +138,7 @@ type raw_red_expr = Genredexpr.raw_red_expr type raw_red_expr = Redexpr.raw_red_expr [%%endif] +[%%if coq = "9.0" || coq = "9.1"] type raw_constant_decl = { name : qualified_name; atts : Attributes.vernac_flags; @@ -146,6 +147,24 @@ type raw_constant_decl = { body : Constrexpr.constr_expr option; red : raw_red_expr option; } +let empty_univ_csts = Univ.Constraints.empty +let dest_udecl ({ UState.univdecl_instance ; univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints } : UState.universe_decl) = + univdecl_extensible_instance, univdecl_extensible_constraints, univdecl_constraints, univdecl_instance +let interp_sort_poly_decl_opt = Constrintern.interp_univ_decl_opt +[%%else] +type raw_constant_decl = { + name : qualified_name; + atts : Attributes.vernac_flags; + udecl : Constrexpr.sort_poly_decl_expr option; + typ : Constrexpr.local_binder_expr list * Constrexpr.constr_expr option; + body : Constrexpr.constr_expr option; + red : raw_red_expr option; +} +let empty_univ_csts = Univ.UnivConstraints.empty +let dest_udecl ({ UState.sort_poly_decl_instance ; sort_poly_decl_extensible_instance; sort_poly_decl_extensible_constraints; sort_poly_decl_univ_constraints } : UState.sort_poly_decl) = + sort_poly_decl_extensible_instance, sort_poly_decl_extensible_constraints, sort_poly_decl_univ_constraints, sort_poly_decl_instance +let interp_sort_poly_decl_opt = Constrintern.interp_sort_poly_decl_opt +[%%endif] type glob_constant_decl_elpi = { name : string list * Names.Id.t; udecl : universe_decl_option; @@ -459,14 +478,13 @@ let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); bod match udecl, poly with | None, false -> state, NotUniversePolymorphic | Some _, false -> nYI "only universe polymorphic definitions can take universe binders" - | None, true -> state, NonCumulative (([],true),(Univ.Constraints.empty,true)) + | None, true -> state, NonCumulative (([],true),(empty_univ_csts,true)) | Some udecl, true -> - let open UState in - let sigma, { univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} = - Constrintern.interp_univ_decl_opt (Rocq_elpi_HOAS.get_global_env state) (Some udecl) in + let sigma, udecl = interp_sort_poly_decl_opt (Rocq_elpi_HOAS.get_global_env state) (Some udecl) in + let sort_poly_decl_extensible_instance, sort_poly_decl_extensible_constraints, sort_poly_decl_univ_constraints, sort_poly_decl_instance = dest_udecl udecl in let ustate = Evd.ustate sigma in let state = merge_universe_context state ustate in - state, NonCumulative ((univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in + state, NonCumulative ((sort_poly_decl_instance,sort_poly_decl_extensible_instance),(sort_poly_decl_univ_constraints,sort_poly_decl_extensible_constraints)) in let sigma = get_sigma state in match body, typ with | Some body, _ -> @@ -497,7 +515,7 @@ let raw_constant_decl_to_glob_synterp ({ name; atts; udecl; typ = (params,typ); let open Attributes in parse polymorphic atts in let udecl = - if poly then NonCumulative (([],true),(Univ.Constraints.empty,true)) + if poly then NonCumulative (([],true),(empty_univ_csts,true)) else NotUniversePolymorphic in state, { name = raw_decl_name_to_glob name; params; typ; udecl; body } @@ -515,14 +533,13 @@ let raw_constant_decl_to_glob glob_sign ({ name; atts; udecl; typ = (params,typ) match udecl, poly with | None, false -> state, NotUniversePolymorphic | Some _, false -> nYI "only universe polymorphic definitions can take universe binders" - | None, true -> state, NonCumulative (([],true),(Univ.Constraints.empty,true)) + | None, true -> state, NonCumulative (([],true),(empty_univ_csts,true)) | Some udecl, true -> - let open UState in - let sigma, { univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} = - Constrintern.interp_univ_decl_opt (Rocq_elpi_HOAS.get_global_env state) (Some udecl) in + let sigma, udecl = interp_sort_poly_decl_opt (Rocq_elpi_HOAS.get_global_env state) (Some udecl) in + let sort_poly_decl_extensible_instance, sort_poly_decl_extensible_constraints, sort_poly_decl_univ_constraints, sort_poly_decl_instance = dest_udecl udecl in let ustate = Evd.ustate sigma in let state = merge_universe_context state ustate in - state, NonCumulative ((univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in + state, NonCumulative ((sort_poly_decl_instance,sort_poly_decl_extensible_instance),(sort_poly_decl_univ_constraints,sort_poly_decl_extensible_constraints)) in state, { name = raw_decl_name_to_glob name; params; typ; udecl; body } let intern_constant_decl glob_sign (it : raw_constant_decl) = glob_sign, it @@ -677,11 +694,11 @@ let mk_indt_decl state univpoly r = match univpoly with | Cmd.Mono -> state, E.mkApp ideclc r [] | Cmd.Poly -> - let state, up, gls = universe_decl.API.Conversion.embed ~depth:0 state (NonCumul(([],true),(Univ.Constraints.empty,true))) in + let state, up, gls = universe_decl.API.Conversion.embed ~depth:0 state (NonCumul(([],true),(Cmd.empty_univ_csts,true))) in assert(gls=[]); state, E.mkApp uideclc r [up] | Cmd.CumulPoly -> - let state, up, gls = universe_decl.API.Conversion.embed ~depth:0 state (Cumul(([],true),(Univ.Constraints.empty,true))) in + let state, up, gls = universe_decl.API.Conversion.embed ~depth:0 state (Cumul(([],true),(Cmd.empty_univ_csts,true))) in assert(gls=[]); state, E.mkApp uideclc r [up] diff --git a/src/rocq_elpi_arg_HOAS.mli b/src/rocq_elpi_arg_HOAS.mli index 26266ee13..770fbe2b6 100644 --- a/src/rocq_elpi_arg_HOAS.mli +++ b/src/rocq_elpi_arg_HOAS.mli @@ -30,6 +30,7 @@ type raw_red_expr = Genredexpr.raw_red_expr type raw_red_expr = Redexpr.raw_red_expr [%%endif] +[%%if coq = "9.0" || coq = "9.1"] type raw_constant_decl = { name : qualified_name; atts : Attributes.vernac_flags; @@ -38,6 +39,17 @@ type raw_constant_decl = { body : Constrexpr.constr_expr option; red : raw_red_expr option; } +[%%else] +type raw_constant_decl = { + name : qualified_name; + atts : Attributes.vernac_flags; + udecl : Constrexpr.sort_poly_decl_expr option; + typ : Constrexpr.local_binder_expr list * Constrexpr.constr_expr option; + body : Constrexpr.constr_expr option; + red : raw_red_expr option; +} +[%%endif] + val pr_raw_constant_decl : Environ.env -> Evd.evar_map -> raw_constant_decl -> Pp.t type glob_constant_decl = Genintern.glob_sign * raw_constant_decl type top_constant_decl = Geninterp.interp_sign * glob_constant_decl diff --git a/src/rocq_elpi_arg_syntax.mlg b/src/rocq_elpi_arg_syntax.mlg index ffa07afdc..007c9de62 100644 --- a/src/rocq_elpi_arg_syntax.mlg +++ b/src/rocq_elpi_arg_syntax.mlg @@ -41,6 +41,14 @@ let streamFail () = raise Gramlib.Stream.Failure let streamOk x = Ok x let streamFail () = Error () [%%endif] + +[%%if coq = "9.0" || coq = "9.1"] +let sort_poly_decl = Procq.Prim.univ_decl +[%%else] +let sort_poly_decl = Procq.Prim.sort_poly_decl +[%%endif] + + } ARGUMENT EXTEND elpi_string PRINTED BY { pr_elpi_string } @@ -311,12 +319,12 @@ GLOB_PRINTED BY { fun _ _ _ -> EA.Cmd.pp_glob env sigma } | [ "Structure" inductive_or_record_definition(id) ] -> { EA.Cmd.RecordDecl (of_coq_record_declaration ~atts:[] Vernacexpr.Structure id) } | [ "#[" attributes(atts) "]" "Structure" inductive_or_record_definition(id) ] -> { EA.Cmd.RecordDecl (of_coq_record_declaration ~atts Vernacexpr.Structure id) } -| [ "Definition" qualified_name(name) univ_decl_opt(udecl) def_body(def) ] -> { of_coq_definition ~loc ~atts:[] name udecl def } -| [ "#[" attributes(atts) "]" "Definition" qualified_name(name) univ_decl_opt(udecl) def_body(def) ] -> { of_coq_definition ~loc ~atts name udecl def } +| [ "Definition" qualified_name(name) sort_poly_decl_opt(udecl) def_body(def) ] -> { of_coq_definition ~loc ~atts:[] name udecl def } +| [ "#[" attributes(atts) "]" "Definition" qualified_name(name) sort_poly_decl_opt(udecl) def_body(def) ] -> { of_coq_definition ~loc ~atts name udecl def } -| [ "Axiom" qualified_name(name) univ_decl_opt(udecl) telescope(typ) colon_constr(t) ] -> { +| [ "Axiom" qualified_name(name) sort_poly_decl_opt(udecl) telescope(typ) colon_constr(t) ] -> { EA.Cmd.(ConstantDecl { name = snd name; atts = []; udecl; typ = (typ,Some t); red = None; body = None }) } -| [ "#[" attributes(atts) "]" "Axiom" qualified_name(name) univ_decl_opt(udecl) telescope(typ) colon_constr(t) ] -> { +| [ "#[" attributes(atts) "]" "Axiom" qualified_name(name) sort_poly_decl_opt(udecl) telescope(typ) colon_constr(t) ] -> { EA.Cmd.(ConstantDecl { name = snd name; atts; udecl; typ = (typ,Some t); red = None; body = None }) } diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 2390510e2..479fabf38 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -352,11 +352,29 @@ let is_mutual_inductive_entry_ground { Entries.mind_entry_params; mind_entry_ind List.for_all (is_ground_rel_ctx_entry sigma) mind_entry_params && List.for_all (is_ground_one_inductive_entry sigma) mind_entry_inds +[%%if coq = "9.0" || coq = "9.1"] +let evd_merge_sort_context_set rigid = Evd.merge_sort_context_set rigid +let global_push_context_set x = Global.push_context_set x +let check_sort_poly_decl = UState.check_univ_decl +let empty_ctxset = Univ.ContextSet.empty +let univ_csts_to_list = Univ.Constraints.elements +let univs_of_csts = UState.constraints +let ucsts_filter = Univ.Constraints.filter +[%%else] +let evd_merge_sort_context_set rigid = Evd.merge_sort_context_set rigid QGraph.Internal +let global_push_context_set x = Global.push_context_set QGraph.Internal x +let check_sort_poly_decl = UState.check_sort_poly_decl +let empty_ctxset = PConstraints.ContextSet.empty +let univ_csts_to_list = Univ.UnivConstraints.elements +let univs_of_csts x = PConstraints.univs @@ UState.constraints x +let ucsts_filter = Univ.UnivConstraints.filter +[%%endif] + let handle_uinst_option_for_inductive ~depth options i state = match options.uinstance with | NoInstance -> let term, ctx = UnivGen.fresh_global_instance (get_global_env state) (GlobRef.IndRef i) in - let state = update_sigma state (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx) in + let state = update_sigma state (fun sigma -> evd_merge_sort_context_set UState.univ_flexible_alg sigma ctx) in snd @@ Constr.destInd term, state, [] | ConcreteInstance i -> i, state, [] | VarInstance (v_head, v_args, v_depth) -> @@ -365,7 +383,7 @@ let handle_uinst_option_for_inductive ~depth options i state = UnivGen.fresh_global_instance (get_global_env state) (GlobRef.IndRef i) in let uinst = snd @@ Constr.destInd term in let state, lp_uinst, extra_goals = uinstance.Conv.embed ~depth state uinst in - let state = update_sigma state (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx) in + let state = update_sigma state (fun sigma -> evd_merge_sort_context_set UState.univ_flexible_alg sigma ctx) in uinst, state, API.Conversion.Unify (v', lp_uinst) :: extra_goals (* FIXME PARTIAL API @@ -601,7 +619,6 @@ let is_global_level env u = match UGraph.check_declared_universes (Environ.universes env) set with | Ok () -> true | Error _ -> false -let global_push_context_set x = Global.push_context_set x let err_if_contains_alg_univ ~depth t = let env = Global.env () in @@ -982,7 +999,7 @@ let add_axiom_or_variable api id ty local_bkind options state = err Pp.(str api ++ str": unsupported attribute @udecl-cumul! or @univpoly-cumul!"); if poly && Option.has_some local_bkind then err Pp.(str api ++ str": section variables cannot be universe polymorphic"); - let univs = UState.check_univ_decl (Evd.ustate sigma) udecl ~poly in + let univs = check_sort_poly_decl (Evd.ustate sigma) udecl ~poly in let kind = Decls.Logical in let impargs = [] in let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in @@ -1002,7 +1019,7 @@ let add_axiom_or_variable api id ty local_bkind options state = ~univs ~impargs ~inline:options.inline ~name end in - let ucsts = match univs with UState.Monomorphic_entry x, _ -> x | _ -> Univ.ContextSet.empty in + let ucsts = match univs with UState.Monomorphic_entry x, _ -> x | _ -> empty_ctxset in gr, ucsts ;; @@ -1504,7 +1521,7 @@ Supported attributes: | ConstRef gref -> let local = options.local <> Some false in Reductionops.ReductionBehaviour.set ~local gref None; - Univ.ContextSet.empty, state, (), [] + empty_ctxset, state, (), [] | _ -> err Pp.(str "reset-simplification must be called on constant")))), DocAbove)] @@ -1704,12 +1721,6 @@ It's a fatal error if Name cannot be located.|})), DocAbove); ] -[%%if coq = "9.0"] -let univ_binder_compat_820 a b = a -[%%else] -let univ_binder_compat_820 a b = b -[%%endif] - [%%if coq = "9.0" || coq= "9.1"] let locality_of_options (o : options) = o.local <> Some false [%%else] @@ -1734,6 +1745,12 @@ let next_name_away_with_default_using_types _ _ id na names ty = let next_name_away_with_default_using_types = Namegen.next_name_away_with_default_using_types [%%endif] +[%%if coq = "9.0" ] +let univ_binder_compat_820 a b = a +[%%else] +let univ_binder_compat_820 a b = b +[%%endif] + let coq_rest_builtins = let open API.BuiltIn in let open Pred in @@ -1890,7 +1907,7 @@ Supported attributes: UnivGen.fresh_global_instance (get_global_env state) (GlobRef.ConstructRef kon) in snd @@ Constr.destConstruct term, update_sigma state - (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx), + (fun sigma -> evd_merge_sort_context_set UState.univ_flexible_alg sigma ctx), [] else UVars.Instance.empty, state, [] @@ -1903,7 +1920,7 @@ Supported attributes: let state, lp_uinst, extra_goals = uinstance.Conv.embed ~depth state uinst in uinst, update_sigma state - (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx), + (fun sigma -> evd_merge_sort_context_set UState.univ_flexible_alg sigma ctx), API.Conversion.Unify (v', lp_uinst) :: extra_goals in let ty = if_keep ty (fun () -> @@ -2398,7 +2415,7 @@ with a number, starting from 1. Full(unit_ctx, "Starts a functor" ^ Rocq_elpi_builtins_synterp.synterp_api_doc)))), (fun name mp params ~depth _ _ -> grab_global_env "coq.env.begin-module-functor" (fun state -> let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_BeginModule (name,mp,params) state in - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocNext); LPCode {| @@ -2422,7 +2439,7 @@ coq.env.begin-module Name MP :- coq.env.begin-module-functor Name MP []. Full(unit_ctx,"Starts a module type functor *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc))), (fun id params ~depth _ _ -> grab_global_env "coq.env.begin-module-type-functor" (fun state -> let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_BeginModuleType (id,params) state in - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocNext); LPCode {| @@ -2450,7 +2467,7 @@ coq.env.begin-module-type Name :- Full(unit_ctx, "Applies a functor *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc))))))), (fun name mp f arguments inline _ ~depth _ _ -> grab_global_env "coq.env.apply-module-functor" (fun state -> let state, mp = Rocq_elpi_builtins_synterp.SynterpAction.pop_ApplyModule (name,mp,f,arguments,inline) state in - Univ.ContextSet.empty, state, ?: mp, []))), + empty_ctxset, state, ?: mp, []))), DocNext); MLCode(Pred("coq.env.apply-module-type-functor", @@ -2462,7 +2479,7 @@ coq.env.begin-module-type Name :- Full(unit_ctx, "Applies a type functor *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc)))))), (fun name f arguments inline _ ~depth _ _ -> grab_global_env "coq.env.apply-module-type-functor" (fun state -> let state, mp = Rocq_elpi_builtins_synterp.SynterpAction.pop_ApplyModuleType (name,f,arguments,inline) state in - Univ.ContextSet.empty, state, ?: mp, []))), + empty_ctxset, state, ?: mp, []))), DocNext); (* XXX When Coq's API allows it, call vernacentries directly *) @@ -2472,7 +2489,7 @@ coq.env.begin-module-type Name :- Full(unit_ctx, "is like the vernacular Include, Inline can be omitted *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc))), (fun mp i ~depth _ _ -> grab_global_env "coq.env.include-module" (fun state -> let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_IncludeModule (mp,i) state in - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); (* XXX When Coq's API allows it, call vernacentries directly *) @@ -2482,7 +2499,7 @@ coq.env.begin-module-type Name :- Full(unit_ctx, "is like the vernacular Include Type, Inline can be omitted *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc))), (fun mp i ~depth _ _ -> grab_global_env "coq.env.include-module-type" (fun state -> let state,_ = Rocq_elpi_builtins_synterp.SynterpAction.pop_IncludeModuleType (mp,i) state in - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.env.import-module", @@ -2490,7 +2507,7 @@ coq.env.begin-module-type Name :- Full(unit_ctx, "is like the vernacular Import *E*")), (fun mp ~depth _ _ -> grab_global_env "coq.env.import-module" (fun state -> let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_ImportModule mp state in - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.env.export-module", @@ -2498,7 +2515,7 @@ coq.env.begin-module-type Name :- Full(unit_ctx, "is like the vernacular Export *E*")), (fun mp ~depth _ _ -> grab_global_env "coq.env.export-module" (fun state -> let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_ExportModule mp state in - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); LPDoc @@ -2522,7 +2539,7 @@ denote the same x as before.|}; Full(unit_ctx, "starts a section named Name *E*")), (fun id ~depth _ _ -> grab_global_env "coq.env.begin-section" (fun state -> let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_BeginSection id state in - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.env.end-section", @@ -2632,12 +2649,12 @@ phase unnecessary.|}; CIn(sort, "S2", Full(global, "constrains S1 <= S2"))), (fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.leq" (fun state -> - if Sorts.equal u1 u2 then Univ.ContextSet.empty, state, (),[] + if Sorts.equal u1 u2 then empty_ctxset, state, (),[] else let state, u2 = if true (* options.algunivs != Some true *) then purge_algebraic_univs_sort state (EConstr.ESorts.make u2) else state, u2 in - Univ.ContextSet.empty, add_universe_constraint state (constraint_leq u1 u2), (),[]))), + empty_ctxset, add_universe_constraint state (constraint_leq u1 u2), (),[]))), DocAbove); MLCode(Pred("coq.sort.eq", @@ -2645,12 +2662,12 @@ phase unnecessary.|}; CIn(sort, "S2", Full(global, "constrains S1 = S2"))), (fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.eq" (fun state -> - if Sorts.equal u1 u2 then Univ.ContextSet.empty, state, (),[] + if Sorts.equal u1 u2 then empty_ctxset, state, (),[] else let state, u2 = if true (* options.algunivs != Some true *) then purge_algebraic_univs_sort state (EConstr.ESorts.make u2) else state, u2 in - Univ.ContextSet.empty, add_universe_constraint state (constraint_eq u1 u2), (), []))), + empty_ctxset, add_universe_constraint state (constraint_eq u1 u2), (), []))), DocAbove); MLCode(Pred("coq.sort.sup", @@ -2742,8 +2759,8 @@ phase unnecessary.|}; (fun _ ~depth _ _ state -> let sigma = get_sigma state in let ustate = Evd.ustate sigma in - let constraints = UState.constraints ustate in - state, !: (Univ.Constraints.elements constraints), [] + let constraints = univs_of_csts ustate in + state, !: (univ_csts_to_list constraints), [] )), DocAbove); @@ -2778,9 +2795,9 @@ phase unnecessary.|}; (fun v _ ~depth _ _ state -> let sigma = get_sigma state in let ustate = Evd.ustate sigma in - let constraints = UState.constraints ustate in - let v_constraints = Univ.Constraints.filter (fun (l1,_,l2) -> Univ.Level.(equal v l1 || equal v l2)) constraints in - state, !: (Univ.Constraints.elements v_constraints), [] + let constraints = univs_of_csts ustate in + let v_constraints = ucsts_filter (fun (l1,_,l2) -> Univ.Level.(equal v l1 || equal v l2)) constraints in + state, !: (univ_csts_to_list v_constraints), [] )), DocAbove); @@ -2966,7 +2983,7 @@ Supported attributes: - @local! (default: false)|})), (fun gr ~depth { options } _ -> grab_global_env "coq.CS.declare-instance" (fun state -> Canonical.declare_canonical_structure ?local:options.local gr; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.CS.db", @@ -3017,7 +3034,7 @@ Supported attributes: (fun gr ~depth { options } _ -> grab_global_env "coq.TC.declare-class" (fun state -> (* CAVEAT: declare_existing_class creates the new class but methods are not added *) Record.declare_existing_class gr; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.elpi.toposort", @@ -3044,7 +3061,7 @@ Supported attributes: let hint_priority = Some priority in Classes.existing_instance global gr (Some { Hints.empty_hint_info with Typeclasses.hint_priority }); - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.TC.db", @@ -3114,7 +3131,7 @@ NParams can always be omitted, since it is inferred. | _, _ -> ComCoercion.try_add_new_coercion gr ~local ~reversible end; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.coercion.db", @@ -3176,7 +3193,7 @@ Supported attributes:|} ^ hint_locality_doc)))), (fun gr (db,_) mode ~depth:_ {options} _ -> grab_global_env "coq.hints.add-mode" (fun state -> let locality = hint_locality options in Hints.add_hints ~locality [db] (Hints.HintsModeEntry(gr,mode)); - Univ.ContextSet.empty, state, (), [] + empty_ctxset, state, (), [] ))), DocAbove); @@ -3203,7 +3220,7 @@ Supported attributes:|} ^ hint_locality_doc)))), let transparent = not opaque in let r = eval_of_constant c in Hints.add_hints ~locality [db] Hints.(HintsTransparencyEntry(HintsReferences [r],transparent)); - Univ.ContextSet.empty, state, (), [] + empty_ctxset, state, (), [] ))), DocAbove); @@ -3233,7 +3250,7 @@ Supported attributes:|} ^ hint_locality_doc))))), let hint_pattern = unspec2opt pattern |> Option.map (Rocq_elpi_utils.detype_to_pattern env sigma) in let info = { Typeclasses.hint_priority; hint_pattern } in Hints.add_hints ~locality [db] Hints.(Hints.HintsResolveEntry[info, true, hint_globref gr]); - Univ.ContextSet.empty, state, (), [] + empty_ctxset, state, (), [] ))), DocAbove); @@ -3266,7 +3283,7 @@ Supported attributes: | B.Unspec -> Anonymous, Glob_term.Explicit | B.Given x -> Anonymous, x))) in Impargs.set_implicits local gref imps; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.arguments.set-default-implicit", @@ -3279,7 +3296,7 @@ Supported attributes: (fun gref ~depth { options } _ -> grab_global_env "coq.arguments.set-default-implicit" (fun state -> let local = options.local <> Some false in Impargs.declare_implicits local gref; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.arguments.name", @@ -3307,7 +3324,7 @@ Supported attributes: | None -> Names.Name.Anonymous | Some x -> Names.(Name.Name (Id.of_string x))) in Arguments_renaming.rename_arguments local gref names; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.arguments.scope", @@ -3332,7 +3349,7 @@ Supported attributes: try ignore (CNotation.find_scope k); k with CErrors.UserError _ -> CNotation.find_delimiters_scope k)) in CNotation.declare_arguments_scope local gref scopes; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLData simplification_strategy; @@ -3363,7 +3380,7 @@ Supported attributes: | ConstRef gref -> let local = options.local <> Some false in compat_reduction_behavior_set ~local gref strategy; - Univ.ContextSet.empty, state, (), [] + empty_ctxset, state, (), [] | _ -> err Pp.(str "set-simplification must be called on constant")))), DocAbove) @@ -3443,7 +3460,7 @@ Supported attributes: let qname = Libnames.qualid_of_string (Id.to_string name) in match Nametab.locate_extended qname with | Globnames.TrueGlobal _ -> assert false - | Globnames.Abbrev sd -> Univ.ContextSet.empty, state, !: sd, []))), + | Globnames.Abbrev sd -> empty_ctxset, state, !: sd, []))), DocAbove); MLCode(Pred("coq.notation.abbreviation", @@ -3533,7 +3550,7 @@ is equivalent to Elpi Export TacName.|})))), let abbrev_name = Rocq_elpi_utils.string_split_on_char '.' name in let tac_name = Rocq_elpi_utils.string_split_on_char '.' tacname in Lib.add_leaf @@ inAbbreviationForTactic { abbrev_name; tac_name; tac_fixed_args}; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLData Rocq_elpi_builtins_synterp.attribute_value; @@ -3902,7 +3919,7 @@ coq.reduction.lazy.whd_all X Y :- let local = ctx.options.local = Some true in let csts = csts |> List.map eval_of_constant in Redexpr.set_strategy local [level, csts]; - Univ.ContextSet.empty, state, (), []))), + empty_ctxset, state, (), []))), DocAbove); MLCode(Pred("coq.strategy.get", @@ -4060,7 +4077,7 @@ Supported attributes: let state, assignments = set_current_sigma ~depth state sigma in (* universe constraints fixed by the code above*) - Univ.ContextSet.empty, state, !: subgoals, assignments + empty_ctxset, state, !: subgoals, assignments ))), DocAbove); @@ -4267,7 +4284,7 @@ Supported attributes: let psl = List.rev (Environ.fold_named_context make_decl_list env ~init:[]) in Pp.(v 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)) in let s = Pp.(repr @@ with_pp_options proof_context.options.pp (fun flags -> - v 0 @@ + v 0 @@ pr_named_context_of flags proof_context.env sigma ++ cut () ++ str "======================" ++ cut () ++ pr_econstr_env_flagged flags proof_context.env sigma