let sort =
(try
Hashtbl.find ids_to_inner_sorts idr
- with Not_found -> `Type) in
+ with Not_found -> `Type (CicUniv.fresh())) in
if sort = `Prop then
K.Premise
{ K.premise_id = gen_id premise_prefix seed;
let sort =
(try
Hashtbl.find ids_to_inner_sorts id
- with Not_found -> `Type) in
+ with Not_found -> `Type (CicUniv.fresh())) in
if sort = `Prop then
K.Lemma
{ K.lemma_id = gen_id lemma_prefix seed;
let sort =
(try
Hashtbl.find ids_to_inner_sorts id
- with Not_found -> `Type) in
+ with Not_found -> `Type (CicUniv.fresh())) in
if sort = `Prop then
let inductive_types =
(let o,_ =
let idarg = get_id arg in
let sortarg =
(try (Hashtbl.find ids_to_inner_sorts idarg)
- with Not_found -> `Type) in
+ with Not_found -> `Type (CicUniv.fresh())) in
let hdarg =
if sortarg = `Prop then
let (co,bo) =
else
let aid = get_id a in
let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
- with Not_found -> `Type) in
+ with Not_found -> `Type (CicUniv.fresh())) in
if asort = `Prop then
K.ArgProof (aux a)
else K.Term a in