* http://helm.cs.unibo.it/
*)
-val add_constant:
- uri:UriManager.uri ->
- ?body:Cic.term -> ty:Cic.term ->
- ugraph:CicUniv.universe_graph ->
- ?params:UriManager.uri list -> ?attrs:Cic.attribute list ->
- MatitaTypes.status -> MatitaTypes.status
+val add_obj:
+ UriManager.uri -> Cic.obj -> MatitaTypes.status -> MatitaTypes.status
+(*
val add_inductive_def:
uri:UriManager.uri ->
types:Cic.inductiveType list ->
?params:UriManager.uri list -> ?leftno:int -> ?attrs:Cic.attribute list ->
ugraph:CicUniv.universe_graph ->
MatitaTypes.status -> MatitaTypes.status
+
+val add_record_def:
+ CicRecord.record_spec ->
+ MatitaTypes.status -> MatitaTypes.status
+*)
val time_travel:
present:MatitaTypes.status -> past:MatitaTypes.status -> unit