| _ -> assert false
let var_has_body uri =
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
| Cic.Variable (_, Some body, _, _, _), _ -> true
| _ -> false
(*assert (not (is_main_pos pos));*)
let set = aux (next_pos pos) set source in
aux (next_pos pos) set target
- | Cic.LetIn (_, term, target) ->
+ | Cic.LetIn (_, term, _, target) ->
if is_main_pos pos then
aux pos set (CicSubstitution.subst term target)
else
| Cic.Lambda (_, source, target) ->
let acc = aux in_hyp acc source in
aux in_hyp acc target
- | Cic.LetIn (_, term, target) ->
+ | Cic.LetIn (_, term, _, target) ->
aux in_hyp acc (CicSubstitution.subst term target)
| Cic.Appl [] -> assert false
| Cic.Appl (hd :: tl) ->
List.length (List.filter (non var_has_body) params)
let rec compute_var pos uri =
- let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
| Cic.Variable (_, Some _, _, _, _) -> S.empty
| Cic.Variable (_, None, ty, params, _) ->
| _ -> assert false
let compute_obj uri =
- let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
| Cic.Variable (_, body, ty, params, _)
| Cic.Constant (_, body, ty, params, _) ->