Adapt to coq/coq#18938 (EConstr.ERelevance)

coq-community · Apr 17, 2024 · f67d47a · f67d47a
1 parent 3d10aec
commit f67d47a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)