From 6c9e2ded8fc093e42902d008a883b6650533d47f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 3 Jun 2014 14:23:17 +0200
Subject: Collecting in Namegen those conventional default names that are used
 in different places

---
 proofs/logic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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)
-- 
cgit v1.2.3