-ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml")
-
-(* 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:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",
- UriManager.uri_of_string "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)",
- UriManager.uri_of_string "cic:/CoRN/algebra/CFields/cf_crr.con"
-
- );
- (
- UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)",
- UriManager.uri_of_string "cic:/CoRN/algebra/CGroups/CGroup.ind#xpointer(1/1)",
- UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/cag_crr.con"
-
- );
-
-]
-;;