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

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7f13fff2cf..475f8d396c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -411,7 +411,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	    let id =
 	      match ty with
 	      | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id
-	      | _ -> Id.of_string "H"
+	      | _ -> default_non_dependent_ident
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
-- 
cgit v1.2.3