From 4d0ef1046012225b44ee5a1768265c52e534109f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 7 Nov 2008 16:55:37 +0000 Subject: [PATCH] Signature_of has been closed with respect to constructors. --- helm/software/components/tactics/metadataQuery.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml index 571a045ad..4beaab5c1 100644 --- a/helm/software/components/tactics/metadataQuery.ml +++ b/helm/software/components/tactics/metadataQuery.ml @@ -171,6 +171,7 @@ let close_with_constructors s metasenv context = List.fold_left (fun (j,s) _ -> let curi = UriManager.uri_of_uriref uri i (Some j) in + prerr_endline ("adding " ^ (UriManager.string_of_uri curi)); j+1,Constr.UriManagerSet.add curi s) (1,s) cl in (i+1,s)) (0,bag) tl) | _ -> assert false) @@ -272,7 +273,8 @@ let signature_of metasenv goal = let ty_set = Constr.constants_of ty in let hyp_set = signature_of_hypothesis context metasenv in let set = Constr.UriManagerSet.union ty_set hyp_set in - close_with_types set metasenv context + close_with_constructors (close_with_types set metasenv context) + metasenv context let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal = -- 2.39.2