X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=9e57f19bc37d35a318e0e2f8d61ab4ae7daece11;hb=ae326f646ef4c01b43d6da04201b427d1e175400;hp=fbe5e4b266018e4e3018fa1f619673ee572eecfc;hpb=538b694e70fafbf298f27cf57cae13928bac95af;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index fbe5e4b26..9e57f19bc 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -87,56 +87,16 @@ let get_obj_and_type_checking_info uri n =
    with
     Not_found ->
      let filename = Getter.getxml uri in
-      let (annobj,_) = CicParser.term_of_xml filename uri false in
-       let obj = Deannotate.deannotate_obj annobj in
-        let output = Unchecked obj in
-         HashTable.add hashtable (uri,0) output ;
-         output
-;;
-
-(* DANGEROUS!!!                                *)
-(* USEFUL ONLY DURING THE FIXING OF THE FILES  *)
-(* change_obj uri (Some newobj)                *)
-(*  maps uri to newobj in cache.               *)
-(* change_obj uri None                         *)
-(*  maps uri to a freeze dummy-object.         *)
-let change_obj uri newobj =
- let newobj =
-  match newobj with
-     Some newobj' -> Unchecked newobj'
-   | None         -> Frozen (Cic.Variable ("frozen-dummy", None, Cic.Implicit))
- in
-  HashTable.remove hashtable (uri,0) ;
-  HashTable.add hashtable (uri,0) newobj
+      let obj = CicParser.obj_of_xml filename uri in
+       let output = Unchecked obj in
+        HashTable.add hashtable (uri,0) output ;
+        output
 ;;
 
 let is_annotation_uri uri =
  Str.string_match (Str.regexp ".*\.ann$") (UriManager.string_of_uri uri) 0
 ;;
 
-(* returns both the annotated and deannotated uncooked forms (plus the *)
-(* map from ids to annotation targets)                                 *)
-let get_annobj_and_type_checking_info uri =
- let filename = Getter.getxml uri in
-  match CicParser.term_of_xml filename uri true with
-     (_, None) -> raise Impossible
-   | (annobj, Some ids_to_targets) ->
-    (* If uri is the uri of an annotation, let's use the annotation file *)
-    if is_annotation_uri uri  then
-(* CSC: la roba annotata non dovrebbe piu' servire
-     AnnotationParser.annotate (Getter.get_ann uri) ids_to_targets ;
-*) assert false ;
-    try
-      (annobj, ids_to_targets, HashTable.find hashtable (uri,0))
-    with
-     Not_found -> 
-      let obj = Deannotate.deannotate_obj annobj in
-       let output = Unchecked obj in
-        HashTable.add hashtable (uri,0) output ;
-        (annobj, ids_to_targets, output)
-;;
-
-
 (* get_obj uri                                                                *)
 (* returns the cic object whose uri is uri. If the term is not just in cache, *)
 (* then it is parsed via CicParser.term_of_xml from the file whose name is    *)
@@ -148,20 +108,6 @@ let get_obj uri =
   | Cooked    obj -> obj
 ;;
 
-(* get_annobj uri                                                             *)
-(* returns the cic object whose uri is uri either in annotated and            *)
-(* deannotated form. The term is put into the cache if it's not there yet.    *)
-let get_annobj uri =
- let (ann, ids_to_targets, deann) = get_annobj_and_type_checking_info uri in
-  let deannobj =
-   match deann with
-      Unchecked obj -> obj
-    | Frozen    _   -> raise (CircularDependency (UriManager.string_of_uri uri))
-    | Cooked    obj -> obj
-  in
-   (ann, ids_to_targets, deannobj)
-;;
-
 (*CSC Commento falso *)
 (* get_obj uri                                                               *)
 (* returns the cooked cic object whose uri is uri. The term must be present  *)