From: Enrico Tassi Date: Fri, 29 Apr 2005 18:52:08 +0000 (+0000) Subject: added the orrible hack to the parser that is needed to call CicUniv.fresh() properly X-Git-Tag: single_binding~128 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d03c83fde2cb3b65e76ea66cd11b4a3cb38192f;p=helm.git added the orrible hack to the parser that is needed to call CicUniv.fresh() properly --- diff --git a/helm/ocaml/cic/cicParser3.mli b/helm/ocaml/cic/cicParser3.mli index 8fc0704d4..b9b8b6d11 100644 --- a/helm/ocaml/cic/cicParser3.mli +++ b/helm/ocaml/cic/cicParser3.mli @@ -62,5 +62,6 @@ class virtual cic_term : (* object that must be linked to it. Used by markup. *) val domspec : cic_term Pxp_document.spec +(** orrible hack *) val set_uri: UriManager.uri -> unit diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index c986ae866..abb50a196 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -941,12 +941,12 @@ let recons_graph graph = MAL.add (recons_univ universe) (recons_entry entry) map) graph MAL.empty -let assert_univs_have_uri graph = - let assert_univ u = +let assert_univ u = match u with | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole") | _ -> () - in + +let assert_univs_have_uri graph = let assert_set s = SOF.iter (fun u -> assert_univ u) s in diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli index 74af1ccc4..3eec9b3be 100644 --- a/helm/ocaml/cic/cicUniv.mli +++ b/helm/ocaml/cic/cicUniv.mli @@ -120,10 +120,16 @@ val restart_numbering: * CicEnvironment.restore_from_channel *) val recons_graph: universe_graph -> universe_graph + (** re-hash-cons a single universe *) +val recons_univ: universe -> universe + (** consistency chek that should be done before committin the graph to the * cache *) val assert_univs_have_uri: universe_graph -> unit + (** asserts the univers is named *) +val assert_univ: universe -> unit + (* Benchmarking stuff *)