From: Claudio Sacerdoti Coen Date: Mon, 19 May 2008 23:06:08 +0000 (+0000) Subject: Added cprop <= type constraint. X-Git-Tag: make_still_working~5141 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a3ff8f4f61a45e8c269322275956fad0805da8bc;p=helm.git Added cprop <= type constraint. --- diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index ab012367a..a793cf059 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -49,6 +49,7 @@ let logger = if debug then prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s)) ;; + let mk_type n = if n = 0 then [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] @@ -56,6 +57,8 @@ let mk_type n = [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] ;; +let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];; + let _ = let do_old_logging = ref true in HelmLogger.register_log_callback @@ -136,6 +139,7 @@ let _ = prerr_endline "finished...."; let lll = List.sort compare (CicUniv.do_rank (get_graph ())) in prerr_endline "caching objects"; + NCicEnvironment.add_constraint true cprop (mk_type 0); let _ = let rec aux = function | a::(b::_ as tl) ->