diff options
Diffstat (limited to 'pretyping/namegen.ml')
| -rw-r--r-- | pretyping/namegen.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index d4435489a..c6c21f025 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -76,9 +76,10 @@ let hdchar env c = | LetIn (_,_,_,c) -> hdrec (k+1) c | Cast (c,_,_) -> hdrec k c | App (f,l) -> hdrec k f - | Const kn -> lowercase_first_char (Label.to_id (con_label kn)) - | Ind x -> lowercase_first_char (basename_of_global (IndRef x)) - | Construct x -> lowercase_first_char (basename_of_global (ConstructRef x)) + | Proj (kn,_) + | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn)) + | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x)) + | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x)) | Var id -> lowercase_first_char id | Sort s -> sort_hdchar s | Rel n -> |