let rec refresh_uri_in_term =
function
+ | NCic.Meta (i,(n,NCic.Ctx l)) ->
+ NCic.Meta (i,(n,NCic.Ctx (List.map refresh_uri_in_term l)))
+ | NCic.Meta _ as t -> t
| NCic.Const (NReference.Ref (u,spec)) ->
NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
| NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l))
type timestamp =
[ `Obj of NUri.uri * NCic.obj
- | `Constr of bool * NCic.universe * NCic.universe] list *
+ | `Constr of NCic.universe * NCic.universe] list *
(NUri.uri * string * NReference.reference) list *
NCic.obj NUri.UriMap.t *
NUri.uri list
let init = load_db;;
+class type g_status =
+ object
+ method timestamp: timestamp
+ end
class status =
object
method timestamp = timestamp
method set_timestamp v = {< timestamp = v >}
method set_library_status
- : 'status. < timestamp : timestamp; .. > as 'status -> 'self
+ : 'status. #g_status as 'status -> 'self
= fun o -> {< timestamp = o#timestamp >}
end
;;
let aliases_of uri =
- try
HExtlib.filter_map
(fun (uri',_,nref) ->
if NUri.eq uri' uri then Some nref else None) !local_aliases
- with
- Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri)))
;;
let add_obj status ((u,_,_,_,_) as obj) =
status#set_timestamp (!storage,!local_aliases,!cache,!includes)
;;
-let add_constraint status strict u1 u2 =
- NCicEnvironment.add_constraint strict u1 u2;
- storage := (`Constr (strict,u1,u2)) :: !storage;
+let add_constraint status u1 u2 =
+ NCicEnvironment.add_lt_constraint u1 u2;
+ storage := (`Constr (u1,u2)) :: !storage;
status#set_timestamp (!storage,!local_aliases,!cache,!includes)
;;