;;
-(* let unification = CicUnification.fo_unif;; *)
+let unification = CicUnification.fo_unif;;
exception MatchingFailure;;
;;
+(*
let equations_blacklist =
List.fold_left
(fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
"cic:/matita/logic/equality/eq_rect.con";
]
;;
+*)
+let equations_blacklist = UriManager.UriSet.empty;;
+
let find_library_equalities dbd context status maxmeta =
let module C = Cic in
let uriset, eqlist =
(List.fold_left
(fun (s, l) (u, e) ->
- if List.exists (meta_convertibility_eq e) l then (
+ if List.exists (meta_convertibility_eq e) (List.map snd l) then (
debug_print
(lazy
(Printf.sprintf "NO!! %s already there!"
(string_of_equality e)));
(UriManager.UriSet.add u s, l)
- ) else (UriManager.UriSet.add u s, e::l))
+ ) else (UriManager.UriSet.add u s, (u, e)::l))
(UriManager.UriSet.empty, []) found)
in
uriset, eqlist, maxm
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-let is_identity ((_, context, ugraph) as env) = function
- | ((_, _, (ty, left, right, _), _, _) as equality) ->
+let is_identity ((metasenv, context, ugraph) as env) = function
+ | ((_, _, (ty, left, right, _), menv, _) as equality) ->
(left = right ||
- (meta_convertibility left right) ||
- (fst (CicReduction.are_convertible context left right ugraph)))
+ (* (meta_convertibility left right) || *)
+ (fst (CicReduction.are_convertible
+ ~metasenv:(metasenv @ menv) context left right ugraph)))
;;