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)",
[] 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 =
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
;;
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
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)")
prerr_endline (UriManager.string_of_uri u);
prerr_endline "")
l
-
+*)
(* EOF *)