(* Copyright (C) 2002, HELM Team.
+
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
in
let consts = MetadataConstraints.constants_of ty in
let b = MetadataConstraints.UriManagerSet.subset consts signature in
+(* if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b) *)
if b then b
else
let ty' = unfold context ty in
let consts' = MetadataConstraints.constants_of ty' in
- MetadataConstraints.UriManagerSet.subset consts' signature
+ let b = MetadataConstraints.UriManagerSet.subset consts' signature in
+(*
+ if not b then prerr_endline ("filtering " ^ (CicPp.ppterm t))
+ else prerr_endline ("keeping " ^ (CicPp.ppterm t));
+*)
+ b
with
| CicTypeChecker.TypeCheckerFailure _ -> assert false
| ProofEngineTypes.Fail _ -> false (* unfold may fail *)
let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
let candidates = get_candidates false universe cache fake_eq in
if dont_filter then candidates
- else
- let candidates = List.filter not_default_eq_term candidates in
- List.filter (only signature context metasenv) candidates
+ else let eq_uri = UriManager.uri_of_uriref eq_uri 0 None in
+ (* let candidates = List.filter not_default_eq_term candidates in *)
+ List.filter
+ (only (MetadataConstraints.UriManagerSet.add eq_uri signature)
+ context metasenv) candidates
let build_equality bag head args proof newmetas maxmeta =
match head with
(lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
let cache = cache_add_list cache context (ct@lt) in
let equations =
- retrieve_equations dont_filter signature universe cache context metasenv
+ retrieve_equations dont_filter (* true *) signature universe cache context metasenv
in
debug_print
(lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));