From 2c2f83bbf8db3869aaf584d6522c3b688bed21bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 19 Sep 2023 15:26:31 +0200 Subject: [PATCH] Adapt to coq/coq#17836 (sort poly) --- graphdepend.mlg | 2 +- searchdepend.mlg | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/graphdepend.mlg b/graphdepend.mlg index 6e6fa20db..2c5e38ec4 100644 --- a/graphdepend.mlg +++ b/graphdepend.mlg @@ -39,7 +39,7 @@ try let t, ctx = Typeops.type_of_global_in_context (Global.env()) gref in (* Beware of this code, not considered entirely correct, but I don't know how to fix it. *) - let env = Environ.push_context ~strict:false (Univ.AbstractContext.repr ctx) + let env = Environ.push_context ~strict:false (UVars.AbstractContext.repr ctx) (Global.env ()) in let s = (Typeops.infer_type env t).Environ.utj_type in Sorts.is_prop s diff --git a/searchdepend.mlg b/searchdepend.mlg index d28a00224..f4a13557d 100644 --- a/searchdepend.mlg +++ b/searchdepend.mlg @@ -50,7 +50,7 @@ let collect_long_names avoid (c:Constr.t) (acc:Data.t) = match kind c with | Var x -> add_identifier x acc | Sort s -> add_sort s acc - | Const cst -> add_constant (Univ.out_punivs cst) acc + | Const cst -> add_constant (UVars.out_punivs cst) acc | Ind (i,_) when not (List.exists (Names.MutInd.CanOrd.equal (fst i)) avoid) -> add_inductive i acc | Construct (cnst,_) when not (List.exists (Names.MutInd.CanOrd.equal (fst (fst cnst))) avoid) -> add_constructor cnst acc | Case({ci_ind=i},_,_,_,_,_,_) ->