From ac11602583c06def887a3cdac736b1d3c57711fc Mon Sep 17 00:00:00 2001 From: Johann Rosain Date: Sun, 23 Nov 2025 18:35:28 +0100 Subject: [PATCH] Adapt to rocq-prover/rocq#21195 (add quality constraint kind) --- src/debug.ml | 2 +- src/declare_translation.ml | 12 ++++++------ src/parametricity.ml | 12 ++++++------ 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/debug.ml b/src/debug.ml index 67ac2ce..010fa07 100644 --- a/src/debug.ml +++ b/src/debug.ml @@ -190,7 +190,7 @@ let debug_mutual_inductive_entry = match entry.mind_entry_universes with | Monomorphic_ind_entry | Template_ind_entry _ -> mt () | Polymorphic_ind_entry ux -> - UVars.pr_universe_context Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes ux + UVars.UContext.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes ux in let mind_entry_cumul_pp = bool (Option.has_some entry.mind_entry_variance) in let mind_entry_private_pp = diff --git a/src/declare_translation.ml b/src/declare_translation.ml index 269b12a..55343f0 100644 --- a/src/declare_translation.ml +++ b/src/declare_translation.ml @@ -114,7 +114,7 @@ let declare_inductive ~opaque_access name ?(continuation = default_continuation) debug_evar_map [`Inductive] "evar_map inductive " env !evd; let size = Declarations.(Array.length mut_body.mind_packets) in let mut_ind_R = DeclareInd.declare_mutual_inductive_with_eliminations translation_entry - (Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders) [] in + (Monomorphic_entry PConstraints.ContextSet.empty, UnivNames.empty_binders) [] in for k = 0 to size-1 do Relations.declare_inductive_relation arity (mut_ind, k) (mut_ind_R, k) done; @@ -245,7 +245,7 @@ and declare_module ~opaque_access ?(continuation = ignore) ?name arity mp mb = let env = Global.env () in let evd = Evd.from_env env in let evd, ucst = - Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst)) + Evd.(with_sort_context_set univ_rigid QGraph.Rigid evd (UnivGen.fresh_constant_instance env cst)) in let evdr = ref evd in ignore(declare_realizer ~opaque_access ~continuation arity evdr env None (mkConstU (fst ucst, EInstance.make (snd ucst)))) @@ -264,7 +264,7 @@ and declare_module ~opaque_access ?(continuation = ignore) ?name arity mp mb = let env = Global.env () in let evd = Evd.from_env env in let evd, ucst = - Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst)) + Evd.(with_sort_context_set univ_rigid QGraph.Rigid evd (UnivGen.fresh_constant_instance env cst)) in let c = mkConstU (fst ucst, EInstance.make (snd ucst)) in let evdr = ref evd in @@ -288,7 +288,7 @@ and declare_module ~opaque_access ?(continuation = ignore) ?name arity mp mb = continuation () else begin let evd, pind = - Evd.(with_sort_context_set univ_rigid !evdr (UnivGen.fresh_inductive_instance env ind)) + Evd.(with_sort_context_set univ_rigid QGraph.Rigid !evdr (UnivGen.fresh_inductive_instance env ind)) in evdr := evd; debug_string [`Module] (Printf.sprintf "inductive field: '%s'." (Names.Label.to_string lab)); @@ -357,7 +357,7 @@ let command_constant ~opaque_access ?(continuation = default_continuation) ~full let scope = Locality.(Global ImportDefaultBehavior) in let kind = Decls.(IsDefinition Definition) in let evd, pconst = - Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env constant)) + Evd.(with_sort_context_set univ_rigid QGraph.Static evd (UnivGen.fresh_constant_instance env constant)) in let constr = mkConstU (fst pconst, EInstance.make @@ snd pconst) in declare_abstraction ~opaque_access ~continuation ~opaque ~poly ~scope ~kind @@ -367,7 +367,7 @@ let command_inductive ~opaque_access ?(continuation = default_continuation) ~ful let env = Global.env () in let evd = Evd.from_env env in let evd, pind = - Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_inductive_instance env inductive)) + Evd.(with_sort_context_set univ_rigid QGraph.Static evd (UnivGen.fresh_inductive_instance env inductive)) in let name = match names with | None -> diff --git a/src/parametricity.ml b/src/parametricity.ml index 6c32512..746a740 100644 --- a/src/parametricity.ml +++ b/src/parametricity.ml @@ -463,7 +463,7 @@ and translate_constant order (evd : Evd.evar_map ref) env cst : constr = Declarations.(match cb.const_body with | Def _ -> let (value, _, constraints) = constant_value_and_type env (kn,names) in - let evd' = Evd.add_constraints !evd constraints in + let evd' = Evd.add_poly_constraints QGraph.Internal !evd constraints in evd := evd'; translate order evd env (of_constr (Option.get value)) | OpaqueDef op -> @@ -1130,12 +1130,12 @@ let fix_template_params order evdr env temp b params = match Univ.Level.var_index u0 with | None -> (* not template, this is technically allowed but dubious *) - Univ.Constraints.add (u0, cst, v) accu + Univ.UnivConstraints.add (u0, cst, v) accu | Some u0 -> match Int.Map.find_opt u0 umap with | None -> assert false (* unbound template level *) | Some (ur, repl) -> - let accu = Univ.Constraints.add (ur, cst, v) accu in - let fold accu u = Univ.Constraints.add (u, cst, v) accu in + let accu = Univ.UnivConstraints.add (ur, cst, v) accu in + let fold accu u = Univ.UnivConstraints.add (u, cst, v) accu in List.fold_left fold accu repl in let uctx = UVars.AbstractContext.repr temp.template_context in @@ -1143,7 +1143,7 @@ let fix_template_params order evdr env temp b params = let qvars, univs = UVars.Instance.to_array univs in let cstrs = UVars.UContext.constraints uctx in let univs = Array.concat @@ Array.map_to_list map_univs univs in - let cstrs = Univ.Constraints.fold fold_cstrs cstrs Univ.Constraints.empty in + let cstrs = PConstraints.fold ((fun _ csts -> csts), fold_cstrs) cstrs PConstraints.empty in let unames = { UVars.quals = Array.make (Array.length qvars) Anonymous; UVars.univs = Array.make (Array.length univs) Anonymous } in let uctx = UVars.UContext.make unames (UVars.Instance.of_array (qvars,univs), cstrs) in let default_univs = @@ -1171,7 +1171,7 @@ let rec translate_mind_body name order evdr env kn b inst = in let r = ERelevance.make ind.mind_relevance in let env = push_rel (toDecl (mkannot (Names.Name typename) r, None, (of_constr full_arity))) env in - let env = Environ.add_constraints cst env in + let env = Environ.add_constraints QGraph.Internal cst env in env ) env (Array.to_list b.mind_packets) in