| Cic.Meta (i, l) -> check_irl 1 l
| Cic.Rel _ -> true
| Cic.Const _ -> true
+ | Cic.MutInd (_, _, []) -> true
+ | Cic.MutConstruct (_, _, _, []) -> true
| _ -> false
;;
let unification metasenv context t1 t2 ugraph =
(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
let subst, menv, ug =
- if not (is_simple_term t1) || not (is_simple_term t2) then
+ if not (is_simple_term t1) || not (is_simple_term t2) then (
+ debug_print (
+ Printf.sprintf "NOT SIMPLE TERMS: %s %s"
+ (CicPp.ppterm t1) (CicPp.ppterm t2));
CicUnification.fo_unif metasenv context t1 t2 ugraph
- else
+ ) else
unification_simple metasenv context t1 t2 ugraph
in
let rec fix_term = function
| None ->
aux newmeta tl
in
- aux maxmeta candidates
+ let found, maxm = aux maxmeta candidates in
+ (List.fold_left
+ (fun l e ->
+ if List.exists (meta_convertibility_eq e) l then (
+ debug_print (
+ Printf.sprintf "NO!! %s already there!" (string_of_equality e));
+ l
+ )
+ else e::l)
+ [] found), maxm
;;