else
[false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
+let mk_cprop n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^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
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) ->
NCicEnvironment.add_constraint true (mk_type a) (mk_type b);
+ NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b);
+ NCicEnvironment.add_constraint true (mk_type a) (mk_cprop a);
+ NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b);
+ NCicEnvironment.add_constraint true (mk_type b) (mk_cprop b);
aux tl
| _ -> ()
in