diff options
| author | Hugo Herbelin | 2014-06-03 14:23:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-04 18:42:22 +0200 |
| commit | 6c9e2ded8fc093e42902d008a883b6650533d47f (patch) | |
| tree | 53b91966c76b3a535308a8a73d113c5fff96de0a /proofs | |
| parent | 90fc6f45fa1a4ef5251046d8b4e4249164afa60b (diff) | |
Collecting in Namegen those conventional default names that are used in different places
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) |