Skip to content

Commit

Permalink
Merge pull request #123 from SkySkimmer/sort-poly
Browse files Browse the repository at this point in the history
Adapt to coq/coq#17836 (sort poly)
  • Loading branch information
ppedrot authored Nov 6, 2023
2 parents 7ac1461 + 2c2f83b commit 85660ac
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion graphdepend.mlg
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion searchdepend.mlg
Original file line number Diff line number Diff line change
Expand Up @@ -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

Check failure on line 53 in searchdepend.mlg

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev)

Unbound module UVars
| 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},_,_,_,_,_,_) ->
Expand Down

0 comments on commit 85660ac

Please sign in to comment.