diff options
Diffstat (limited to 'pretyping/namegen.ml')
| -rw-r--r-- | pretyping/namegen.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 6c490d7b9..8b9e6e633 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -38,7 +38,6 @@ let default_type_ident = Id.of_string default_type_string let default_non_dependent_string = "H" let default_non_dependent_ident = Id.of_string default_non_dependent_string -let default_dependent_string = "x" let default_dependent_ident = Id.of_string "x" (**********************************************************************) |