- raise (U.UnificationFailure "Inference.unification.unif")
-(* | C.Meta (i, l), C.Meta (j, l') -> *)
-(* let _, _, ty = CicUtil.lookup_meta i menv in *)
-(* let _, _, ty' = CicUtil.lookup_meta j menv in *)
-(* let binding1 = lookup s subst in *)
-(* let binding2 = lookup t subst in *)
-(* let subst, menv = *)
-(* if binding1 != s then *)
-(* if binding2 != t then *)
-(* unif subst menv binding1 binding2 *)
-(* else *)
-(* if binding1 = t then *)
-(* subst, menv *)
-(* else *)
-(* ((j, (context, binding1, ty'))::subst, *)
-(* List.filter (fun (m, _, _) -> j <> m) menv) *)
-(* else *)
-(* if binding2 != t then *)
-(* if s = binding2 then *)
-(* subst, menv *)
-(* else *)
-(* ((i, (context, binding2, ty))::subst, *)
-(* List.filter (fun (m, _, _) -> i <> m) menv) *)
-(* else *)
-(* ((i, (context, t, ty))::subst, *)
-(* List.filter (fun (m, _, _) -> i <> m) menv) *)
-(* in *)
-(* subst, menv *)
-
- | C.Meta (i, l), t ->
- let _, _, ty = CicUtil.lookup_meta i menv in
- let subst =
- if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
- else subst
- in
- let menv = List.filter (fun (m, _, _) -> i <> m) menv in
- subst, menv
+ raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
+ | C.Meta (i, l), t -> (
+ try
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ let subst =
+ if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
+ else subst
+ in
+ let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
+ subst, menv
+ with CicUtil.Meta_not_found m ->
+ let names = names_of_context context in
+ debug_print (lazy (
+ Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
+ (CicPp.pp t1 names) (CicPp.pp t2 names)
+ (print_metasenv menv) (print_metasenv metasenv)));
+ assert false
+ )