Skip to content

Commit

Permalink
Adapt to coq/coq#18938 (EConstr.ERelevance)
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Apr 17, 2024
1 parent eb307d8 commit b7afbb5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/wp_eauto.ml
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ let e_assumption: trace tactic =
Tacticals.tclZEROMSG (str "No applicable tactic.")
else
let not_ground = occur_existential sigma concl in
let map (decl: ('a, types) Declaration.pt): trace tactic =
let map (decl: (_, types, _) Declaration.pt): trace tactic =
let id = Declaration.get_id decl in
let t = Declaration.get_type decl in
begin
Expand Down

0 comments on commit b7afbb5

Please sign in to comment.