From f67d47ae8479145a97608401e481df0d638454bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 17 Apr 2024 14:12:36 +0200 Subject: [PATCH] Adapt to coq/coq#18938 (EConstr.ERelevance) --- src/staltac_lib.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/staltac_lib.ml b/src/staltac_lib.ml index 9f88a3a..cf6c5df 100644 --- a/src/staltac_lib.ml +++ b/src/staltac_lib.ml @@ -239,7 +239,7 @@ let convertConcl sigma cl = (* Convert the hashtable into a function array *) let buildEnv hash = let acc = ref (mkApp ((Lazy.force coq_rArrayInitP) - ,[| mkLambda (Context.make_annot Names.Anonymous Sorts.Relevant, (Lazy.force coq_rNat), + ,[| mkLambda (Context.make_annot Names.Anonymous ERelevance.relevant, (Lazy.force coq_rNat), (Lazy.force coq_True)) |])) in ConstrMap.iter (fun c n -> acc := (mkApp ((Lazy.force coq_rArraySetP)