From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- kernel/names.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index b349ccb0..480b37e8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -33,9 +33,9 @@ struct let hash = String.hash - let check_soft x = + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then Errors.error x else Pp.msg_warning (str x) + if fatal then Errors.error x else if warn then Pp.msg_warning (str x) in Option.iter iter (Unicode.ident_refutation x) @@ -48,6 +48,11 @@ struct let s = String.copy s in String.hcons s + let of_string_soft s = + let () = check_soft ~warn:false s in + let s = String.copy s in + String.hcons s + let to_string id = String.copy id let print id = str id @@ -571,7 +576,6 @@ let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) -let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i -- cgit v1.2.3