parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / metadataQuery.ml

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index 571a045adfbfd54b2833bcaf0a13aaa6b5d97197..6db568cb4ab9ad60516bc30f1a0d366e4e6a7b1f 100644 (file)
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -171,6 +171,8 @@ 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 +274,10 @@ 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_types
+     (close_with_constructors (close_with_types set metasenv context)
+       metasenv context)
+    metasenv context
 
 
 let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =