From d2d0007efa611a000b37ad6583f1052a023b9e19 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 30 Aug 2005 10:15:44 +0000 Subject: [PATCH] Bug fixed: "cic:/dummy_i" is an invalid URI (that used to be erroneously accepted by the getter). Changed to "cic:/dummy_i.con". --- helm/ocaml/tactics/metadataQuery.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 9355dfc10..9f0cff9ad 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -415,7 +415,7 @@ let fill_with_dummy_constants t = function Cic.Lambda (n,s,t) -> let dummy_uri = - UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)) in + UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in (aux (i+1) (s::types) (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) | t -> t,types @@ -444,7 +444,7 @@ let instance ~dbd t = when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") -> let s = UriManager.string_of_uri s in let len = String.length s in - let dummy_index = int_of_string (String.sub s 11 (len-11)) in + let dummy_index = int_of_string (String.sub s 11 (len-15)) in let dummy_type = List.nth types dummy_index in Some (d,dummy_type) | _::l -> look_for_dummy_main l -- 2.39.2