let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
let mk_type n =
- if n = 0 then
- [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
- else
- [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [`Type, 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")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
else
- [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
let is_proof_irrelevant context ty =
match CicReduction.whd context tty with
Cic.MutInd (_,_,ens) -> ens,[]
| Cic.Appl (Cic.MutInd (_,_,ens)::args) ->
- ens,fst (HExtlib.split_nth "ON 1" leftno args)
+ ens,fst (HExtlib.split_nth leftno args)
| _ -> assert false
in
let rec aux n irl context outsort =
in
let obj =
nuri_of_ouri buri,0,[],[],
- NCic.Fixpoint (false, fl, (`Generated, `Definition))
+ NCic.Fixpoint (false, fl, (`Generated, `Definition, `Regular))
in
let r = reference_of_ouri buri (Ref.CoFix cofixno) in
let obj,r =
in
let obj =
nuri_of_ouri buri,height,[],[],
- NCic.Fixpoint (true, fl, (`Generated, `Definition)) in
+ NCic.Fixpoint (true, fl, (`Generated, `Definition, `Regular)) in
(*prerr_endline ("H(" ^ UriManager.string_of_uri buri ^ ") = " ^ string_of_int * height);*)
let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,height)) in
let obj,r =
aux false [] [] 0 uri t
;;
*)
+
+let reference_of_oxuri u =
+ let t = CicUtil.term_of_uri u in
+ let t',l = convert_term (UriManager.uri_of_string "cic:/dummy/dummy.con") t in
+ match t',l with
+ NCic.Const nref, [] -> nref
+ | _,_ -> assert false
+;;