From af805d8cb199ea2c532983e29b064cf9861454f4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 May 2009 14:50:27 +0000 Subject: [PATCH] Constructors are closed with thier types when computing the signatur --- 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 f12cd9a19..6db568cb4 100644 --- a/helm/software/components/tactics/metadataQuery.ml +++ b/helm/software/components/tactics/metadataQuery.ml @@ -274,7 +274,9 @@ 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_constructors (close_with_types set metasenv context) + close_with_types + (close_with_constructors (close_with_types set metasenv context) + metasenv context) metasenv context -- 2.39.2