From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 30 Aug 2005 10:15:44 +0000 (+0000)
Subject: Bug fixed: "cic:/dummy_i" is an invalid URI (that used to be erroneously accepted... 
X-Git-Tag: working_equations_only~10
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d2d0007efa611a000b37ad6583f1052a023b9e19;p=helm.git

Bug fixed: "cic:/dummy_i" is an invalid URI (that used to be erroneously accepted by the getter). Changed to "cic:/dummy_i.con".
---

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