Skip to content

Commit

Permalink
Keeping the '__'
Browse files Browse the repository at this point in the history
  • Loading branch information
Stevendeo committed Oct 19, 2023
1 parent 80ef91a commit 5205d8a
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
3 changes: 1 addition & 2 deletions src/lib/structures/expr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1712,10 +1712,9 @@ let skolemize { main = f; binders; sko_v; sko_vty; _ } =
let tyvars = Format.asprintf "[%a]" pp_list sko_vty in

let mk_sym cpt s =
(* garder le suffixe "__" car cela influence l'ordre *)
Fmt.kstr
(fun str -> Sy.make_as_fresh_skolem str)
"__%s%s!%d"
"%s%s!%d"
s
tyvars
cpt
Expand Down
3 changes: 2 additions & 1 deletion src/lib/structures/symbols.ml
Original file line number Diff line number Diff line change
Expand Up @@ -392,7 +392,8 @@ module MakeId(S : sig val prefix : string end) : Id = struct
end

module InternalId = MakeId(struct let prefix = "!k" end)
module SkolemId = MakeId(struct let prefix = "!?" end)
module SkolemId = MakeId(struct let prefix = "!?__" end)
(* garder le suffixe "__" car cela influence l'ordre *)

let fresh_internal_string () = InternalId.fresh ()
let fresh_internal_name () = name (fresh_internal_string ())
Expand Down

0 comments on commit 5205d8a

Please sign in to comment.