Use of standard OCaml syntax

[helm.git] / matita / components / ng_library / nCicLibrary.mli

diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli
index 63589694ad4f3f51cdefc4b14bc2e6a6f3942f5f..14090cdcb9614d0b65ff01fd676d37c24bba87dc 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.mli
+++ b/matita/components/ng_library/nCicLibrary.mli
@@ -21,12 +21,14 @@ class virtual status :
   inherit NCic.status
   method timestamp: timestamp
   method set_timestamp: timestamp -> 'self
+  (*CSC: bug here, we are not copying the NCicExtraction and OCamlExtraction part of the status *)
  end
 
 (* it also checks it and add it to the environment *)
-val add_obj: #status as 'status -> NCic.obj -> 'status
+val add_obj: (#status as 'status) -> NCic.obj -> 'status
 val add_constraint: 
-  #status as 'status -> NCic.universe -> NCic.universe -> 'status
+  (#status as 'status) -> acyclic:bool ->
+  NCic.universe -> NCic.universe -> 'status
 val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
 (*
@@ -35,6 +37,7 @@ val get_obj: #NCic.status -> NUri.uri -> NCic.obj (* changes the current timesta
 *)
 
 val time_travel: #status -> unit
+val replace: #status -> unit
 
 val init: unit -> unit
 
@@ -54,7 +57,7 @@ class dumpable_status :
  end
 
 val get_transitively_included: #dumpable_status -> NUri.uri list
-val dump_obj: #dumpable_status as 'status -> obj -> 'status
+val dump_obj: (#dumpable_status as 'status) -> obj -> 'status
 
 module type SerializerType =
  sig
@@ -76,7 +79,7 @@ module type SerializerType =
   val dependencies_of: baseuri:NUri.uri -> string list
  end
 
-module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status  val set: dumpable_s -> dumpable_status -> dumpable_s end) :
+module Serializer(D: sig type dumpable_s = private #dumpable_status end) :
   SerializerType with type dumpable_status = D.dumpable_s
 
 val refresh_uri: NUri.uri -> NUri.uri