aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
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