let empty_db = DB.empty ;;
let add_user_provided_hint db t precedence =
- let u = UriManager.uri_of_string "cic:/foo/bar.con" in
let c, a, b =
let rec aux ctx = function
| NCic.Appl l ->
(match List.rev l with
| b::a::_ -> ctx, a, b
| _ -> assert false)
- | NCic.Prod (n,s,t) ->
- aux ((n, NCic.Decl s) :: ctx) t
- | NCic.LetIn (n,ty,t,b) ->
- aux ((n, NCic.Def (t,ty)) :: ctx) b
+ | NCic.Prod (n,s,t) -> aux ((n, NCic.Decl s) :: ctx) t
+ | NCic.LetIn (n,ty,t,b) -> aux ((n, NCic.Def (t,ty)) :: ctx) b
| _ -> assert false
in
- aux [] (fst (OCic2NCic.convert_term u t))
+ aux [] t
in
index_hint db c a b precedence
;;