From b7afbb530a7017ddbc864b0c30e219daf39457f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 17 Apr 2024 14:17:46 +0200 Subject: [PATCH] Adapt to coq/coq#18938 (EConstr.ERelevance) --- src/wp_eauto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/wp_eauto.ml b/src/wp_eauto.ml index 51716f94..f19e3758 100644 --- a/src/wp_eauto.ml +++ b/src/wp_eauto.ml @@ -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