let xxx_type_of_aux' m c t =
let t1 = Sys.time () in
- let res = CicTypeChecker.type_of_aux' m c t in
+ let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
let t2 = Sys.time () in
type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
res
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri with
- CicEnvironment.CheckedObj cobj -> cobj
+ match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+ CicEnvironment.CheckedObj (cobj,_) -> cobj
| CicEnvironment.UncheckedObj uobj ->
raise (NotWellTyped "Reference to an unchecked constant")
in
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- match CicEnvironment.is_type_checked uri with
- CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
+ match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+ CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),_) -> ty
| CicEnvironment.UncheckedObj (C.Variable _) ->
raise (NotWellTyped "Reference to an unchecked variable")
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri with
- CicEnvironment.CheckedObj cobj -> cobj
+ match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+ CicEnvironment.CheckedObj (cobj,_) -> cobj
| CicEnvironment.UncheckedObj uobj ->
raise (NotWellTyped "Reference to an unchecked inductive type")
in
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri with
- CicEnvironment.CheckedObj cobj -> cobj
+ match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+ CicEnvironment.CheckedObj (cobj,_) -> cobj
| CicEnvironment.UncheckedObj uobj ->
raise (NotWellTyped "Reference to an unchecked constructor")
in
(* Checks suppressed *)
CicSubstitution.lift_meta l ty
| C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
- let t' = CicUniv.fresh() in
- if not (CicUniv.add_gt t' t ) then
- assert false (* t' is fresh! an error in CicUniv *)
- else
- C.Sort (C.Type t')
+ C.Sort (C.Type (CicUniv.fresh()))
| C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
| C.Implicit _ -> raise (Impossible 21)
| C.Cast (te,ty) ->
(* Checks suppressed *)
(* Let's visit all the subterms that will not be visited later *)
let (cl,parsno) =
- let obj =
+ let obj,_ =
try
- CicEnvironment.get_cooked_obj uri
+ CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
with Not_found -> assert false
in
match obj with
and visit_exp_named_subst context uri exp_named_subst =
let uris_and_types =
- let obj =
+ let obj,_ =
try
- CicEnvironment.get_cooked_obj uri
+ CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
with Not_found -> assert false
in
match obj with
| Cic.InductiveDefinition (_,params,_) ->
List.map
(function uri ->
- let obj =
+ let obj,_ =
try
- CicEnvironment.get_cooked_obj uri
+ CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
with Not_found -> assert false
in
match obj with
(* different from Coq manual!!! *)
C.Sort s2
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
- let t' = CicUniv.fresh() in
- if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
- assert false ; (* not possible, error in CicUniv *)
- C.Sort (C.Type t')
+ C.Sort (C.Type (CicUniv.fresh()))
| (C.Sort _,C.Sort (C.Type t1)) ->
(* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)