Skip to content

Commit 48f6e56

Browse files
authored
Merge pull request #189 from SkySkimmer/nolab
Adapt to rocq-prover/rocq#21174 (rm Label)
2 parents 757a929 + 34c5589 commit 48f6e56

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/wp_rewrite.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,7 @@ let fresh_key: unit -> KerName.t =
232232
let (mp, _) = KerName.repr kn in
233233
let lbl = Id.of_string_soft (Printf.sprintf "%s#%i"
234234
(ModPath.to_string mp) cur)
235-
in KerName.make mp (Label.of_id lbl)
235+
in KerName.make mp lbl
236236

237237
let decompose_applied_relation (env: Environ.env) (sigma: Evd.evar_map) (c: constr) (ctype: Evd.econstr) (left2right: bool): hypinfo option =
238238
let find_rel ty =

0 commit comments

Comments
 (0)