try
let ty,_ =
CicTypeChecker.type_of_aux'
- metasenv current_ctx t CicUniv.empty_ugraph
+ metasenv current_ctx t CicUniv.oblivion_ugraph
in
let sort,_ =
CicTypeChecker.type_of_aux'
- metasenv current_ctx ty CicUniv.empty_ugraph
+ metasenv current_ctx ty CicUniv.oblivion_ugraph
in
let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in
match sort with
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ =
- CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph
in
let ty_sort2,_ =
- CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.oblivion_ugraph
in
let prop1 =
let b,_ =
CicReduction.are_convertible
- ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph
+ ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.oblivion_ugraph
in
if b then 0
else 1
let prop2 =
let b,_ =
CicReduction.are_convertible
- ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph
+ ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.oblivion_ugraph
in
if b then 0
else 1
(fun e bag ->
let t = CicUtil.term_of_uri e in
let ty, _ =
- CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
in
Constr.UriManagerSet.union bag (Constr.constants_of ty))
s s
match t with
Cic.MutInd (uri,_,_)
| Cic.MutConstruct (uri,_,_,_) ->
- (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
Cic.InductiveDefinition(tl,_,_,_) ->
snd
(List.fold_left
List.fold_left
(fun (j,s) _ ->
let curi = UriManager.uri_of_uriref uri i (Some j) in
+(* prerr_endline ("adding " ^
+ * (UriManager.string_of_uri curi)); *)
j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
(i+1,s)) (0,bag) tl)
| _ -> assert false)
let is_predicate u =
let ty, _ =
try CicTypeChecker.type_of_aux' [] []
- (CicUtil.term_of_uri u) CicUniv.empty_ugraph
+ (CicUtil.term_of_uri u) CicUniv.oblivion_ugraph
with CicTypeChecker.TypeCheckerFailure _ -> assert false
in
let rec check_last_pi = function
let only constants uri =
prerr_endline (UriManager.string_of_uri uri);
let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
- let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
let consts = Constr.constants_of ty in
(*
prerr_endline ("XXX " ^ UriManager.string_of_uri uri);
(fun (i,acc) _ ->
let ty, _ =
CicTypeChecker.type_of_aux'
- metasenv context (Cic.Rel i) CicUniv.empty_ugraph in
+ metasenv context (Cic.Rel i) CicUniv.oblivion_ugraph in
let newty = types_of_equality ty in
(i+1,Constr.SetSet.union newty acc))
(1,all) context
let ty_set = Constr.constants_of ty in
let hyp_set = signature_of_hypothesis context metasenv in
let set = Constr.UriManagerSet.union ty_set hyp_set in
- close_with_types set metasenv context
+ close_with_types
+ (close_with_constructors (close_with_types set metasenv context)
+ metasenv context)
+ metasenv context
let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
| Some (main,_) ->
let ty, _ =
CicTypeChecker.type_of_aux'
- metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
+ metasenv context (CicUtil.term_of_uri main)
+ CicUniv.oblivion_ugraph
in
Constr.constants_of ty
in