diff options
Diffstat (limited to 'pretyping/namegen.ml')
| -rw-r--r-- | pretyping/namegen.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 245c7f943..a6c0149a4 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -83,7 +83,7 @@ let head_name c = (* Find the head constant of a constr if any *) match kind_of_term c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) | Cast (c,_,_) | App (c,_) -> hdrec c - | Proj (kn,_) -> Some (Label.to_id (con_label kn)) + | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn))) | Const _ | Ind _ | Construct _ | Var _ -> Some (basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> @@ -104,7 +104,7 @@ let hdchar env c = match kind_of_term c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c | Cast (c,_,_) | App (c,_) -> hdrec k c - | Proj (kn,_) + | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant 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)) |