Merge pull request #31 from SkySkimmer/erelevance

Adapt to coq/coq#18938 (EConstr.ERelevance)
coq-community · Apr 23, 2024 · d32acd3 · d32acd3
2 parents 3d10aec + f67d47a
commit d32acd3
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)