let rec process_type_aux kind =
function
C.Var (uri,expl_named_subst) ->
- ([!!!kind, UriManager.string_of_uri uri],[],[]) @@
+ (* andrea: this is a bug: variable are not indexedin the db
+ ([!!!kind, UriManager.string_of_uri uri],[],[]) @@ *)
(process_type_aux_expl_named_subst kind expl_named_subst)
| C.Rel _ ->
(match kind with
match s with
Cic.Prop -> T.Prop
| Cic.Set -> T.Set
- | Cic.Type -> T.Type
+ | Cic.Type _ -> T.Type (* TASSI: ?? *)
| Cic.CProp -> T.CProp
in
[],[],[!!kind,s']
| _ -> [],[],[])
- | C.Meta _
+ | C.Meta _ -> [],[],[] (* ???? To be understood *)
| C.Implicit _ -> assert false
| C.Cast (te,_) ->
(* type ignored *)
;;
(*CSC: Debugging only *)
+(*
let get_constraints term =
let res = get_constraints term in
let (objs,rels,sorts) = res in
(function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s)
) sorts ;
res
-;;
+;; *)
let universe =
[T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]