implemented elim query

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
+

diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli
index 6bea094a44de7ad9fc994b7831607df2f9aa5caf..2a97a283fa4ff321be88dc5807233d3886b29634 100644 (file)
--- 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