From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Oct 2004 14:50:55 +0000 (+0000)
Subject: implemented elim query
X-Git-Tag: V_0_0_10~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d8dec8837c8f459bfb7d7e6182cfbd34d869ab2;p=helm.git

implemented elim query
---

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index cbca9a9c2..d280b0928 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -152,3 +152,13 @@ List.iter prerr_endline uris;
   in
   aux uris
 
+let elim ~dbh uri =
+  let constraints =
+    [`Rel [`MainConclusion None];
+     `Sort (Cic.Prop,[`MainHypothesis (Some 1)]);
+     `Obj (uri,[`MainHypothesis (Some 0)]);
+     `Obj (uri,[`InHypothesis]);
+    ]
+  in
+  MetadataConstraints.at_least ~dbh constraints
+
diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli
index 6bea094a4..2a97a283f 100644
--- a/helm/ocaml/tactics/metadataQuery.mli
+++ b/helm/ocaml/tactics/metadataQuery.mli
@@ -33,5 +33,5 @@ val hint:
 
 val match_term: dbh:Dbi.connection -> Cic.term -> string list
 
-(* val elim: dbh:Dbi.connection -> string -> string list *)
+val elim: dbh:Dbi.connection -> string -> string list