diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/termops.ml | 11 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 |
3 files changed, 5 insertions, 11 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 164043cf7c..ba2d2fdf39 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -658,8 +658,8 @@ let rec subst_rawconstr subst raw = let ref',_ = subst_global subst ref in if ref' == ref then raw else RHole (loc,InternalHole) - | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | - InternalHole | TomatchTypeParameter _ | GoalEvar)) -> raw + | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole | + TomatchTypeParameter _ | GoalEvar | ImpossibleCase)) -> raw | RCast (loc,r1,k) -> (match k with diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 6d8946f440..227a4f9ed0 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -684,12 +684,8 @@ let subst_term_occ_decl locs c (id,bodyopt,typ as d) = (* First character of a constr *) -let first_char id = - let id = string_of_id id in - assert (id <> ""); - String.make 1 id.[0] - -let lowercase_first_char id = String.lowercase (first_char id) +let lowercase_first_char id = + lowercase_first_char_utf8 (string_of_id id) let vars_of_env env = let s = @@ -718,8 +714,7 @@ let hdchar env c = | Cast (c,_,_) -> hdrec k c | App (f,l) -> hdrec k f | Const kn -> - let c = lowercase_first_char (id_of_label (con_label kn)) in - if c = "?" then "y" else c + lowercase_first_char (id_of_label (con_label kn)) | Ind ((kn,i) as x) -> if i=0 then lowercase_first_char (id_of_label (label kn)) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 608a7d9dbd..aa814442ab 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -151,7 +151,6 @@ val eta_reduce_head : constr -> constr val eta_eq_constr : constr -> constr -> bool (* finding "intuitive" names to hypotheses *) -val first_char : identifier -> string val lowercase_first_char : identifier -> string val sort_hdchar : sorts -> string val hdchar : env -> types -> string |