From 648d1495bb71b72169bc67c78071600b82a5bfda Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Jun 2006 11:51:08 +0000 Subject: [PATCH] ancient bug solved. if the term is (eq TY A B) the signature of A and B was ignored if TY was a Sort. --- components/metadata/metadataConstraints.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/components/metadata/metadataConstraints.ml b/components/metadata/metadataConstraints.ml index 07fcc738b..6cab493fc 100644 --- a/components/metadata/metadataConstraints.ml +++ b/components/metadata/metadataConstraints.ml @@ -384,7 +384,7 @@ let rec signature_of = function Some (u, []), add l | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> let suri = UriManager.uri_of_uriref u t None in - if u = HelmLibraryObjects.Logic.eq_URI then + if LibraryObjects.is_eq_URI u then (* equality is handled in a special way: in particular, the type, if defined, is always added to the prefix, and n is not decremented - it should have been n-2 *) @@ -400,7 +400,7 @@ let rec signature_of = function let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in let inconcl = UriManagerSet.remove suri1 (add l1) in Some (suri, [suri1]), inconcl - | _ :: _ -> Some (suri, []), UriManagerSet.empty + | _ :: tl -> Some (suri, []), add tl | _ -> assert false (* args number must be > 0 *) else Some (suri, []), add l @@ -541,7 +541,7 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) List.map (fun uri -> (card, uri)) res)) maximal_prefixes) in - Printf.fprintf stderr "all: %d\n" (List.length all);flush_all (); +(* Printf.fprintf stderr "all: %d\n" (List.length all);flush_all (); *) List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in greater_than @ equal_to -- 2.39.2