diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 08354ef556..d5086df1a3 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -313,7 +313,7 @@ let name_prop_vars env sigma ctxt = List.map2 (fun (na,b,t as d) s -> if na = Anonymous && s = prop_sort then let s = match Namegen.head_name t with Some id -> string_of_id id | None -> "" in - (Name (add_suffix (id_of_string "H") s),b,t) + (Name (add_suffix Namegen.default_prop_ident s),b,t) else d) ctxt (sorts_of_context env sigma ctxt) |