X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=6aad3676d11176fa045cc26ebfed4df9190b92cb;hb=de4483296d06aac3df4da10d5401b1f97c4350ab;hp=4dd05073b26b3ab2af09899254f7713a6a25a22c;hpb=93e7f6e653ae9e6e17d054ccd3b9aaf801e13bcf;p=helm.git

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index 4dd05073b..6aad3676d 100644
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,13 +25,13 @@
 
 open Printf;;
 
-ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml")
+type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
 
 (* the list of known coercions (MUST be transitively closed) *)
 let coercions = ref [
   (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",
    UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con",
-   UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ;
+   UriManager.uri_of_string "cic:/Coq/Reals/Raxioms/INR.con") ;
 
    (
      UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",
@@ -94,7 +94,7 @@ let get_closure_coercions src tgt uri =
     [] c_to_src)
 ;;
 
-      
+let obj_attrs = [`Class `Coercion; `Generated]
 
 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
 let generate_composite_closure c1 c2 univ =
@@ -129,7 +129,7 @@ let generate_composite_closure c1 c2 univ =
   let cleaned_ty =
     FreshNamesGenerator.clean_dummy_dependent_types c_ty 
   in
-  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[]) in 
+  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in 
     obj,univ
 ;;
 
@@ -161,13 +161,14 @@ let close_coercion_graph src tgt uri =
                 CicUtil.term_of_uri (UriManager.string_of_uri uri)
               in
               let first_step = 
-                (Cic.Constant ("",Some (term_of_uri' he),Cic.Sort Cic.Prop,[]))
+                Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
+                  obj_attrs)
               in
               let o,u = 
                 List.fold_left (fun (o,u) coer ->
                   match o with 
-                  |  Cic.Constant (_,Some c,_,[]) ->
-                    generate_composite_closure c (term_of_uri' coer) u
+                  | Cic.Constant (_,Some c,_,[],_) ->
+                      generate_composite_closure c (term_of_uri' coer) u
                   | _ -> assert false 
                 ) (first_step, CicUniv.empty_ugraph) tl
               in
@@ -180,21 +181,23 @@ let close_coercion_graph src tgt uri =
               in
               let named_obj = 
                 match o with
-                | Cic.Constant (_,bo,ty,vl) -> Cic.Constant (name,bo,ty,vl)
+                | Cic.Constant (_,bo,ty,vl,attrs) ->
+                    Cic.Constant (name,bo,ty,vl,attrs)
                 | _ -> assert false 
               in
                 ((src,tgt,c_uri),(c_uri,named_obj,u))
       ) todo_list)
   in
-  coercions := !coercions @ new_coercions;
+  coercions := !coercions @ new_coercions @ [src,tgt,uri];
   new_coercions_obj
 ;;
 
-
+let get_coercions_list () =
+  !coercions
 
 
 (* stupid case *)
-
+(*
 let l = close_coercion_graph 
  (UriManager.uri_of_string
  "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)")
@@ -208,7 +211,7 @@ in
    prerr_endline (UriManager.string_of_uri u);
    prerr_endline "")
  l
- 
+*) 
  
 
 (* EOF *)