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},_,_,_,_,_,_) ->