From 87e3427435d3e120cc0292764a93a68b6daddd4a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 9 Feb 2007 16:18:37 +0000 Subject: [PATCH] Avoid generating invalid names with "'" in the middle of them. --- .../components/cic_proof_checking/freshNamesGenerator.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml index 4838623c2..3cfda02df 100755 --- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml +++ b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml @@ -93,7 +93,7 @@ let mk_fresh_name ~subst metasenv context name ~typ = with CicTypeChecker.TypeCheckerFailure _ -> "H" ) | C.Name name -> - Str.global_replace (Str.regexp "[0-9]*$") "" name + Str.global_replace (Str.regexp "[0-9']*$") "" name in let already_used name = List.exists (function Some (n,_) -> n=name | _ -> false) context -- 2.39.2