[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")];;
+
(* porcatissima *)
type reference = Ref of NUri.uri * NReference.spec
let reference_of_ouri u indinfo =
let ty, fixpoints_ty = aux k octx ctx n_fix uri ty in
NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
| Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
- | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
+ | Cic.Sort Cic.CProp -> NCic.Sort (NCic.Type cprop),[]
| Cic.Sort (Cic.Type u) ->
NCic.Sort (NCic.Type (mk_type (CicUniv.get_rank u))),[]
| Cic.Sort Cic.Set -> NCic.Sort (NCic.Type (mk_type 0)),[]
NCic.Const (reference_of_ouri curi Ref.Decl)
| _ -> assert false)
| Cic.MutInd (curi, tyno, ens) ->
- let is_inductive =
+ let is_inductive, lno =
match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
- Cic.InductiveDefinition ([],_,_,_) -> true
- | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+ Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+ | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
| _ -> assert false
in
aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
+ (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno))))
| Cic.MutConstruct (curi, tyno, consno, ens) ->
+ let lno =
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+ Cic.InductiveDefinition (_,_,lno,_) -> lno
+ | _ -> assert false
+ in
aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno))))
+ (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno,lno))))
| Cic.Var (curi, ens) ->
(match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
Cic.Variable (_,Some bo,_,_,_) ->
aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
| _ -> assert false)
| Cic.MutCase (curi, tyno, outty, t, branches) ->
- let is_inductive =
+ let is_inductive,lno =
match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
- Cic.InductiveDefinition ([],_,_,_) -> true
- | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+ Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+ | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
| _ -> assert false in
- let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
+ let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno)) in
let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
let t, fixpoints_t = aux k octx ctx n_fix uri t in
let branches, fixpoints =
let is_proof_irrelevant context ty =
match
- fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
+ CicReduction.whd context
+ (fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph))
with
Cic.Sort Cic.Prop -> true
| Cic.Sort _ -> false