Skip to content

Commit

Permalink
Merge pull request #122 from herbelin/coq-master+adapt-coq-pr17987-se…
Browse files Browse the repository at this point in the history
…arch-pass-sigma

Adapt to Coq PR #17987 which adds sigma to the API of search functions
  • Loading branch information
ppedrot authored Sep 8, 2023
2 parents 3433d7e + edc3a43 commit 7ac1461
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions graphdepend.mlg
Original file line number Diff line number Diff line change
Expand Up @@ -26,12 +26,12 @@ let filename = ref "graph.dpd"

let get_dirlist_grefs dirlist =
let selected_gref = ref [] in
let select gref kind env constr =
if Search.module_filter (SearchInside dirlist) gref kind env (Evd.from_env env) constr then
let select gref kind env sigma constr =
if Search.module_filter (SearchInside dirlist) gref kind env sigma constr then
(debug (str "Select " ++ Printer.pr_global gref);
selected_gref := gref::!selected_gref)
in
Search.generic_search (Global.env()) select;
Search.generic_search (Global.env()) (Evd.from_env (Global.env())) select;

Check failure on line 34 in graphdepend.mlg

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev)

This function has type Environ.env -> Search.display_function -> unit
!selected_gref

let is_prop gref id =
Expand Down

0 comments on commit 7ac1461

Please sign in to comment.