implemented elim query

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index cbca9a9c270304d6feb62fee26b580e39da551cf..d280b0928ee0b074f28f8d2a79f596df94ea6bd6 100644 (file)
--- 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
+