diff options
| author | herbelin | 2008-05-10 15:38:36 +0000 |
|---|---|---|
| committer | herbelin | 2008-05-10 15:38:36 +0000 |
| commit | 7df139ca0834b0b93e6259eaecb05c0b8c5cbe99 (patch) | |
| tree | 730574f70b420f85d0836a75b03f820bebfa619b /pretyping | |
| parent | 19b041bcc069e79608392d705fa9998440d50815 (diff) | |
- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des
noms illégaux si le type auquel elle s'appliquait n'était pas pur ascii).
[util.ml, termops.ml]
- Simplification de la procédure d'initialisation (apparemment des résidus
obsolètes de la V5.10) et messages d'erreurs [lib.ml, toplevel.ml, coqtop.ml]
- Quelques pattern-matching incomplets [topconstr.ml, detyping.ml]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10916 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |