From dfb64dda51f7eea174e41129c8d2e0c3559298ec Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 16 Apr 2015 08:35:57 +0200 Subject: Fixing bug #4190. The solution is a bit ugly. In order for two tactic notations identifiers not to be confused by the inclusion from two distinct modules, we embed the name of the source module in the identifiers. This may still fail if the same module is included twice with two distinct parameters, but this should not be possible thanks to the fact any definition in there will forbid the inclusion, for it would be repeated. People including twice the same empty module otherwise probably deserve whatever will arise from it. --- kernel/names.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index 4ccf5b60a..480b37e89 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 -- cgit v1.2.3